Mathlib.Order.RelIso.Set

RelHomClass.map_inf theorem

 [SemilatticeInf α] [LinearOrder β] [FunLike F β α] [RelHomClass F (· < ·) (· < ·)] (a : F) (m n : β) :
  a (m ⊓ n) = a m ⊓ a n

Full source

theorem map_inf [SemilatticeInf α] [LinearOrder β] [FunLike F β α]
    [RelHomClass F (· < ·) (· < ·)] (a : F) (m n : β) :
    a (m ⊓ n) = a m ⊓ a n :=
  (StrictMono.monotone fun _ _ => map_rel a).map_inf m n

Preservation of Infima by Strict Order-Preserving Maps

Informal description

Let $\alpha$ be a semilattice with infima (meets), $\beta$ a linear order, and $F$ a type of functions from $\beta$ to $\alpha$ that preserves the strict order relation $<$ (i.e., $f \in F$ implies $x < y \Rightarrow f(x) < f(y)$). Then for any $f \in F$ and any $m, n \in \beta$, the function $f$ preserves meets, i.e., $f(m \sqcap n) = f(m) \sqcap f(n)$.

RelHomClass.map_sup theorem

 [SemilatticeSup α] [LinearOrder β] [FunLike F β α] [RelHomClass F (· > ·) (· > ·)] (a : F) (m n : β) :
  a (m ⊔ n) = a m ⊔ a n

Full source

theorem map_sup [SemilatticeSup α] [LinearOrder β] [FunLike F β α]
    [RelHomClass F (· > ·) (· > ·)] (a : F) (m n : β) :
    a (m ⊔ n) = a m ⊔ a n :=
  map_inf (α := αᵒᵈ) (β := βᵒᵈ) _ _ _

Preservation of Joins by Strict Order-Reversing Maps

Informal description

Let $\alpha$ be a semilattice with suprema (joins), $\beta$ a linear order, and $F$ a type of functions from $\beta$ to $\alpha$ that preserves the strict order relation $>$ (i.e., $f \in F$ implies $x > y \Rightarrow f(x) > f(y)$). Then for any $f \in F$ and any $m, n \in \beta$, the function $f$ preserves joins, i.e., $f(m \sqcup n) = f(m) \sqcup f(n)$.

RelHomClass.directed theorem

[FunLike F α β] [RelHomClass F r s] {ι : Sort*} {a : ι → α} {f : F} (ha : Directed r a) : Directed s (f ∘ a)

Full source

theorem directed [FunLike F α β] [RelHomClass F r s] {ι : Sort*} {a : ι → α} {f : F}
    (ha : Directed r a) : Directed s (f ∘ a) :=
  ha.mono_comp _ fun _ _ h ↦ map_rel f h

Preservation of Directedness under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ with a relation homomorphism structure `RelHomClass F r s`, where $r$ is a relation on $\alpha$ and $s$ is a relation on $\beta$. Given a directed family of elements $(a_i)_{i \in \iota}$ in $\alpha$ with respect to $r$ (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $r(a_i, a_k)$ and $r(a_j, a_k)$ hold), the composition $f \circ a$ is directed with respect to $s$ in $\beta$.

RelHomClass.directedOn theorem

[FunLike F α β] [RelHomClass F r s] {f : F} {t : Set α} (hs : DirectedOn r t) : DirectedOn s (f '' t)

Full source

theorem directedOn [FunLike F α β] [RelHomClass F r s] {f : F}
    {t : Set α} (hs : DirectedOn r t) : DirectedOn s (f '' t) :=
  hs.mono_comp fun _ _ h ↦ map_rel f h

Image of Directed Set under Relation Homomorphism is Directed

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ equipped with a relation homomorphism structure `RelHomClass F r s`, where $r$ is a relation on $\alpha$ and $s$ is a relation on $\beta$. Given a subset $t \subseteq \alpha$ that is directed with respect to $r$ (i.e., for any $x, y \in t$, there exists $z \in t$ such that $r(x,z)$ and $r(y,z)$ hold), the image $f(t)$ is directed with respect to $s$ in $\beta$.

RelIso.range_eq theorem

(e : r ≃r s) : Set.range e = Set.univ

Full source

theorem range_eq (e : r ≃r s) : Set.range e = Set.univ := by simp

Range of Relation Isomorphism is Universal Set

Informal description

For any relation isomorphism $e$ between relations $r$ and $s$, the range of $e$ is equal to the universal set of the target type.

Subrel definition

(r : α → α → Prop) (p : α → Prop) : Subtype p → Subtype p → Prop

Full source

/-- `Subrel r p` is the inherited relation on a subtype.

We could also consider a Set.Subrel r s variant for dot notation, but this ends up interacting
poorly with `simpNF`. -/
def Subrel (r : α → α → Prop) (p : α → Prop) : Subtype p → Subtype p → Prop :=
  Subtype.valSubtype.val ⁻¹'o r

Subtype relation

Informal description

Given a relation $r$ on a type $\alpha$ and a predicate $p$ on $\alpha$, the `Subrel r p` is the restriction of the relation $r$ to the subtype of elements satisfying $p$. Specifically, for two elements $a$ and $b$ in the subtype, $(\text{Subrel}\ r\ p)\ a\ b$ holds if and only if $r\ a.1\ b.1$ holds, where $a.1$ and $b.1$ are the underlying elements of $\alpha$. In other words, $\text{Subrel}\ r\ p$ is the relation induced by $r$ on the subset of $\alpha$ defined by $p$.

subrel_val theorem

(r : α → α → Prop) (p : α → Prop) {a b} : Subrel r p a b ↔ r a.1 b.1

Full source

@[simp]
theorem subrel_val (r : α → α → Prop) (p : α → Prop) {a b} : SubrelSubrel r p a b ↔ r a.1 b.1 :=
  Iff.rfl

Characterization of Subtype Relation via Underlying Elements

Informal description

For any relation $r$ on a type $\alpha$ and predicate $p$ on $\alpha$, and for any elements $a$ and $b$ in the subtype defined by $p$, the relation $\text{Subrel}\ r\ p$ holds between $a$ and $b$ if and only if $r$ holds between their underlying elements $a.1$ and $b.1$ in $\alpha$.

Subrel.relEmbedding definition

(r : α → α → Prop) (p : α → Prop) : Subrel r p ↪r r

Full source

/-- The relation embedding from the inherited relation on a subset. -/
protected def relEmbedding (r : α → α → Prop) (p : α → Prop) : SubrelSubrel r p ↪r r :=
  ⟨Embedding.subtype _, Iff.rfl⟩

Relation embedding from a subtype relation to the original relation

Informal description

Given a relation $r$ on a type $\alpha$ and a predicate $p$ on $\alpha$, the function `Subrel.relEmbedding` constructs a relation embedding from the restricted relation $\text{Subrel}\ r\ p$ (the relation $r$ restricted to the subtype of elements satisfying $p$) back to the original relation $r$. This embedding maps each element of the subtype to its underlying element in $\alpha$ and preserves the relation structure, meaning that for any two elements $a$ and $b$ in the subtype, $(\text{Subrel}\ r\ p)\ a\ b$ holds if and only if $r\ a.1\ b.1$ holds.

Subrel.relEmbedding_apply theorem

(r : α → α → Prop) (p a) : Subrel.relEmbedding r p a = a.1

Full source

@[simp]
theorem relEmbedding_apply (r : α → α → Prop) (p a) : Subrel.relEmbedding r p a = a.1 :=
  rfl

Underlying Element Mapping in Subtype Relation Embedding

Informal description

For any relation $r$ on a type $\alpha$ and predicate $p$ on $\alpha$, the relation embedding $\text{Subrel.relEmbedding}\ r\ p$ maps an element $a$ of the subtype defined by $p$ to its underlying element $a.1$ in $\alpha$.

Subrel.inclusionEmbedding definition

(r : α → α → Prop) {s t : Set α} (h : s ⊆ t) : Subrel r (· ∈ s) ↪r Subrel r (· ∈ t)

Full source

/-- `Set.inclusion` as a relation embedding. -/
protected def inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) :
    SubrelSubrel r (· ∈ s) ↪r Subrel r (· ∈ t) where
  toFun := Set.inclusion h
  inj' _ _ h := (Set.inclusion_inj _).mp h
  map_rel_iff' := Iff.rfl

Relation embedding induced by set inclusion

Informal description

Given a relation $r$ on a type $\alpha$ and two subsets $s \subseteq t$ of $\alpha$, the function `Subrel.inclusionEmbedding` constructs a relation embedding from the restriction of $r$ to $s$ (denoted $\text{Subrel}\ r\ (\cdot \in s)$) to the restriction of $r$ to $t$ (denoted $\text{Subrel}\ r\ (\cdot \in t)$). This embedding is realized by the set inclusion function $\text{Set.inclusion}\ h : s \to t$, where $h$ is the proof that $s \subseteq t$. The embedding preserves the relation structure, meaning that for any $x, y \in s$, $r\ x\ y$ holds in $s$ if and only if $r\ (\text{Set.inclusion}\ h\ x)\ (\text{Set.inclusion}\ h\ y)$ holds in $t$.

Subrel.coe_inclusionEmbedding theorem

(r : α → α → Prop) {s t : Set α} (h : s ⊆ t) : (Subrel.inclusionEmbedding r h : s → t) = Set.inclusion h

Full source

@[simp]
theorem coe_inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) :
    (Subrel.inclusionEmbedding r h : s → t) = Set.inclusion h :=
  rfl

Equality of Inclusion Embedding and Set Inclusion Function

Informal description

For any relation $r$ on a type $\alpha$ and subsets $s \subseteq t$ of $\alpha$, the underlying function of the relation embedding $\text{Subrel.inclusionEmbedding}\ r\ h$ (where $h$ is the proof that $s \subseteq t$) is equal to the set inclusion function $\text{Set.inclusion}\ h : s \to t$.

Subrel.instIsReflSubtype instance

(r : α → α → Prop) [IsRefl α r] (p : α → Prop) : IsRefl _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsRefl α r] (p : α → Prop) : IsRefl _ (Subrel r p) :=
  ⟨fun x => @IsRefl.refl α r _ x⟩

Reflexivity of Subtype Relations

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ is also reflexive.

Subrel.instIsSymmSubtype instance

(r : α → α → Prop) [IsSymm α r] (p : α → Prop) : IsSymm _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsSymm α r] (p : α → Prop) : IsSymm _ (Subrel r p) :=
  ⟨fun x y => @IsSymm.symm α r _ x y⟩

Symmetry of Restricted Relations

Informal description

For any symmetric relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ on the subtype of elements satisfying $p$ is also symmetric.

Subrel.instIsAsymmSubtype instance

(r : α → α → Prop) [IsAsymm α r] (p : α → Prop) : IsAsymm _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsAsymm α r] (p : α → Prop) : IsAsymm _ (Subrel r p) :=
  ⟨fun x y => @IsAsymm.asymm α r _ x y⟩

Asymmetry of Restricted Relations

Informal description

For any relation $r$ on a type $\alpha$ that is asymmetric, and any predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ on the subtype of elements satisfying $p$ is also asymmetric.

Subrel.instIsTransSubtype instance

(r : α → α → Prop) [IsTrans α r] (p : α → Prop) : IsTrans _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsTrans α r] (p : α → Prop) : IsTrans _ (Subrel r p) :=
  ⟨fun x y z => @IsTrans.trans α r _ x y z⟩

Transitivity of Restricted Relation on Subtype

Informal description

For any transitive relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restriction of $r$ to the subtype of elements satisfying $p$ is also transitive.

Subrel.instIsIrreflSubtype instance

(r : α → α → Prop) [IsIrrefl α r] (p : α → Prop) : IsIrrefl _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsIrrefl α r] (p : α → Prop) : IsIrrefl _ (Subrel r p) :=
  ⟨fun x => @IsIrrefl.irrefl α r _ x⟩

Irreflexivity of Subtype Relations

Informal description

For any type $\alpha$ with an irreflexive relation $r$ and a predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ on the subtype of elements satisfying $p$ is also irreflexive.

Subrel.instIsTrichotomousSubtype instance

(r : α → α → Prop) [IsTrichotomous α r] (p : α → Prop) : IsTrichotomous _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsTrichotomous α r] (p : α → Prop) : IsTrichotomous _ (Subrel r p) :=
  ⟨fun x y => by rw [Subtype.eq_iff]; exact @IsTrichotomous.trichotomous α r _ x y⟩

Trichotomy of Subtype Relations

Informal description

For any relation $r$ on a type $\alpha$ that is trichotomous (i.e., for any two elements $x$ and $y$ in $\alpha$, exactly one of $r\ x\ y$, $x = y$, or $r\ y\ x$ holds), and any predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ on the subtype of elements satisfying $p$ is also trichotomous.

Subrel.instIsWellFoundedSubtype instance

(r : α → α → Prop) [IsWellFounded α r] (p : α → Prop) : IsWellFounded _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsWellFounded α r] (p : α → Prop) : IsWellFounded _ (Subrel r p) :=
  (Subrel.relEmbedding r p).isWellFounded

Well-foundedness of Subtype Relations

Informal description

For any well-founded relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restricted relation $\text{Subrel}\ r\ p$ on the subtype of elements satisfying $p$ is also well-founded.

Subrel.instIsPreorderSubtype instance

(r : α → α → Prop) [IsPreorder α r] (p : α → Prop) : IsPreorder _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsPreorder α r] (p : α → Prop) : IsPreorder _ (Subrel r p) where

Restriction of Preorder to Subtype is Preorder

Informal description

For any preorder relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restriction of $r$ to the subtype of elements satisfying $p$ is also a preorder.

Subrel.instIsStrictOrderSubtype instance

(r : α → α → Prop) [IsStrictOrder α r] (p : α → Prop) : IsStrictOrder _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsStrictOrder α r] (p : α → Prop) : IsStrictOrder _ (Subrel r p) where

Restriction of Strict Order to Subtype is Strict Order

Informal description

For any strict order relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restriction of $r$ to the subtype of elements satisfying $p$ is also a strict order.

Subrel.instIsWellOrderSubtype instance

(r : α → α → Prop) [IsWellOrder α r] (p : α → Prop) : IsWellOrder _ (Subrel r p)

Full source

instance (r : α → α → Prop) [IsWellOrder α r] (p : α → Prop) : IsWellOrder _ (Subrel r p) where

Restriction of Well-Order to Subtype is Well-Order

Informal description

For any well-order relation $r$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the restriction of $r$ to the subtype of elements satisfying $p$ is also a well-order.

RelEmbedding.codRestrict definition

(p : Set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r Subrel s (· ∈ p)

Full source

/-- Restrict the codomain of a relation embedding. -/
def RelEmbedding.codRestrict (p : Set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r Subrel s (· ∈ p) :=
  ⟨f.toEmbedding.codRestrict p H, f.map_rel_iff'⟩

Codomain restriction of a relation embedding

Informal description

Given a relation embedding $f$ from $r$ to $s$, a subset $p$ of $\beta$, and a proof $H$ that for every element $a$, $f(a)$ is in $p$, the function constructs a relation embedding from $r$ to the restriction of $s$ to the subset $p$. In other words, it restricts the codomain of the relation embedding $f$ to the subset $p$ while preserving the embedding properties.

RelEmbedding.codRestrict_apply theorem

(p) (f : r ↪r s) (H a) : RelEmbedding.codRestrict p f H a = ⟨f a, H a⟩

Full source

@[simp]
theorem RelEmbedding.codRestrict_apply (p) (f : r ↪r s) (H a) :
    RelEmbedding.codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

Application of Codomain-Restricted Relation Embedding

Informal description

Given a relation embedding $f$ from $r$ to $s$, a subset $p$ of $\beta$, and a proof $H$ that for every element $a$, $f(a) \in p$, the application of the codomain-restricted embedding $\text{RelEmbedding.codRestrict}\ p\ f\ H$ to an element $a$ yields the pair $\langle f(a), H(a) \rangle$.

RelIso.image_eq_preimage_symm theorem

(e : r ≃r s) (t : Set α) : e '' t = e.symm ⁻¹' t

Full source

theorem RelIso.image_eq_preimage_symm (e : r ≃r s) (t : Set α) : e '' t = e.symm ⁻¹' t :=
  e.toEquiv.image_eq_preimage t

Relation Isomorphism Image Equals Inverse Preimage

Informal description

For any relation isomorphism $e$ between relations $r$ and $s$, and any subset $t$ of the domain type $\alpha$, the image of $t$ under $e$ is equal to the preimage of $t$ under the inverse isomorphism $e^{-1}$. In symbols: $e(t) = e^{-1}{-1}(t)$.

RelIso.preimage_eq_image_symm theorem

(e : r ≃r s) (t : Set β) : e ⁻¹' t = e.symm '' t

Full source

theorem RelIso.preimage_eq_image_symm (e : r ≃r s) (t : Set β) : e ⁻¹' t = e.symm '' t := by
  rw [e.symm.image_eq_preimage_symm]; rfl

Preimage-Image Symmetry for Relation Isomorphisms

Informal description

For any relation isomorphism $e$ between relations $r$ and $s$, and any subset $t$ of the codomain type $\beta$, the preimage of $t$ under $e$ is equal to the image of $t$ under the inverse isomorphism $e^{-1}$. In symbols: $e^{-1}(t) = e^{-1}(t)$.

Acc.of_subrel theorem

{r : α → α → Prop} [IsTrans α r] {b : α} (a : { a // r a b }) (h : Acc (Subrel r (r · b)) a) : Acc r a.1

Full source

theorem Acc.of_subrel {r : α → α → Prop} [IsTrans α r] {b : α} (a : { a // r a b })
    (h : Acc (Subrel r (r · b)) a) : Acc r a.1 :=
  h.recOn fun a _ IH ↦ ⟨_, fun _ hb ↦ IH ⟨_, _root_.trans hb a.2⟩ hb⟩

Accessibility Lifting from Subrelation to Original Relation

Informal description

Let $r$ be a transitive relation on a type $\alpha$, and let $b$ be an element of $\alpha$. For any element $a$ in the subtype $\{a \mid r(a, b)\}$, if $a$ is accessible with respect to the restricted relation $\text{Subrel}\ r\ (r(\cdot, b))$, then the underlying element $a.1$ is accessible with respect to the original relation $r$.

wellFounded_iff_wellFounded_subrel theorem

{r : α → α → Prop} [IsTrans α r] : WellFounded r ↔ ∀ b, WellFounded (Subrel r (r · b))

Full source

/-- A relation `r` is well-founded iff every downward-interval `{ a | r a b }` of it is
well-founded. -/
theorem wellFounded_iff_wellFounded_subrel {r : α → α → Prop} [IsTrans α r] :
    WellFoundedWellFounded r ↔ ∀ b, WellFounded (Subrel r (r · b)) where
  mp h _ := InvImage.wf Subtype.val h
  mpr h := ⟨fun a ↦ ⟨_, fun b hr ↦ ((h a).apply _).of_subrel ⟨b, hr⟩⟩⟩

Well-foundedness Characterization via Downward-interval Restrictions

Informal description

A transitive relation $r$ on a type $\alpha$ is well-founded if and only if for every element $b \in \alpha$, the restricted relation $\text{Subrel}\ r\ (r(\cdot, b))$ (i.e., $r$ restricted to the set $\{a \mid r(a, b)\}$) is well-founded.