RelHom.injective_of_increasing
theorem RelHom.injective_of_increasing :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous α r]
[inst : IsIrrefl β s] (f : r →r s), Function.Injective ⇑f
The theorem `RelHom.injective_of_increasing` states that for any types `α` and `β`, and any relations `r` on `α` and `s` on `β`, if `α` is trichotomous under `r` and `β` is irreflexive under `s`, then any relation-preserving function `f` from `r` to `s` is injective. In other words, if `f` is a function that preserves the order properties of `r` and `s`, then it has the property that if `f(x) = f(y)`, it must be the case that `x = y`.
More concisely: If relations `r` on type `α` are trichotomous and `s` on type `β` are irreflexive, then any relation-preserving function `f` from `r` to `s` is injective.
|
WellFounded.quotient_lift₂
theorem WellFounded.quotient_lift₂ :
∀ {α : Type u_1} [inst : Setoid α] {r : α → α → Prop}
{H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
WellFounded r → WellFounded (Quotient.lift₂ r H)
This theorem, named `WellFounded.quotient_lift₂`, is about the property of "well-foundedness" in the context of binary relations and quotients. It states that for any given type `α` with a corresponding `Setoid` instance, a binary relation `r` on `α`, and a proof `H` that `r` respects the equivalence relation defined by the `Setoid`, if the original binary relation `r` is well-founded, then its lifted version onto the quotients `Quotient.lift₂ r H` is also well-founded. In other words, the well-foundedness property is preserved when lifting a binary relation to a quotient using `Quotient.lift₂`. Here, a relation is well-founded if there are no infinite descending chains, i.e., one can't keep finding `a`'s such that `r a b` holds for an already found `b`.
More concisely: If `α` is a type with a `Setoid` instance, `r` is a well-founded binary relation on `α`, and `H` is a proof that `r` respects the equivalence relation defined by the `Setoid`, then `Quotient.lift₂ r H` is a well-founded binary relation on the quotient of `α` by the equivalence relation.
|
WellFounded.of_quotient_liftOn₂'
theorem WellFounded.of_quotient_liftOn₂' :
∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop}
{H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → r a₁ a₂ = r b₁ b₂},
(WellFounded fun x y => x.liftOn₂' y r H) → WellFounded r
This theorem, named `WellFounded.of_quotient_liftOn₂'`, establishes a condition under which a binary relation `r` on a type `α` is well-founded. The condition is that a well-founded relation can be constructed via `liftOn₂'` function on the quotient set by a specified setoid `s`, where the `liftOn₂'` function is defined such that it preserves the relation `r` under the equivalence relation `Setoid.r` of the setoid `s`. That is, the relation `r` between any two elements `a₁, a₂` of type `α` is the same as the relation between any two elements `b₁, b₂` that are equivalent to `a₁, a₂` respectively under the setoid's equivalence relation. If such a well-founded relation can be constructed, then the original relation `r` is well-founded.
More concisely: If the relation `r` on type `α` is preserved under the `liftOn₂'` function of a well-founded setoid `s` on `α`, then `r` is a well-founded relation.
|
RelIso.apply_symm_apply
theorem RelIso.apply_symm_apply :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β), e (e.symm x) = x := by
sorry
This theorem states that for any types `α` and `β`, any relations `r` on `α` and `s` on `β`, and any relation isomorphism `e` from `r` to `s`, if we apply the inverse of `e` to an element `x` of `β`, then apply `e` to the result, we get back `x`. This essentially asserts that the `RelIso.symm` function is the true inverse of a relation isomorphism, in compliance with the property of an inverse function.
More concisely: For any relation isomorphisms `e : r ≃ s` between relations `r` on type `α` and `s` on type `β`, `e (e⁻¹ x) = x` for all `x : β`.
|
RelIso.map_rel_iff'
theorem RelIso.map_rel_iff' :
∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r ≃r s) {a b : α},
s (self.toEquiv a) (self.toEquiv b) ↔ r a b
This theorem states that for any types `α` and `β`, and any binary relations `r` on `α` and `s` on `β`, if a relational isomorphism (or `RelIso`) exists from `r` to `s`, then any pair of elements `a` and `b` of type `α` are related under `r` if and only if their images under the isomorphism are related under `s`. In other words, the relational isomorphism preserves the relational properties between elements from the original set to the image set.
More concisely: If `RelIso` `f` exists from binary relation `r` on type `α` to binary relation `s` on type `β`, then for all `a ∈ α` and `b ∈ β`, `a` `R` `b` if and only if `f a` `S` `f b`, where `R` is the relation symbol for `r` and `S` is the relation symbol for `s`.
|
RelEmbedding.map_rel_iff
theorem RelEmbedding.map_rel_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (f a) (f b) ↔ r a b
This theorem states that for any two types `α` and `β`, and any two relations `r` on `α` and `s` on `β`, and a relation-preserving embedding `f` from `r` into `s`, for any `a` and `b` of type `α`, `s (f a) (f b)` is true if and only if `r a b` is true. In other words, a relation holds between two elements in the original space if and only if the same relation holds between their images in the target space under a relation-preserving embedding.
More concisely: For any relation-preserving embedding `f` between types `α` and `β` and relations `r` on `α` and `s` on `β`, `r(a, b)` implies `s(f a, f b)` and vice versa, for all `a, b` in `α`.
|
RelEmbedding.coe_fn_injective
theorem RelEmbedding.coe_fn_injective :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
The theorem `RelEmbedding.coe_fn_injective` states that for any types `α` and `β`, and for any relations `r` on `α` and `s` on `β`, the function that maps a relation embedding (a function `f : α → β` that preserves the relation structure) to its underlying function (the function that just maps `α` to `β`, without considering the relation structure) is injective. In other words, if two relation embeddings from `r` to `s` have the same effect when applied to elements of `α`, then they must be the same embedding.
More concisely: If two functions between types are relation embeddings with the same underlying function between their source and target types, then they are equal as functions.
|
RelEmbedding.wellFounded
theorem RelEmbedding.wellFounded :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → WellFounded s → WellFounded r := by
sorry
This theorem states that for any two types `α` and `β`, and any two relations `r` on `α` and `s` on `β`, if `r` is a relational embedding of `s` (i.e., `r ↪r s`), and if `s` is well-founded (meaning there is no infinite decreasing sequence), then `r` must also be well-founded. In other words, relational embedding preserves the property of well-foundedness from one relation to another.
More concisely: If `r` is a relational embedding of well-founded relation `s`, then `r` is a well-founded relation.
|
injective_of_increasing
theorem injective_of_increasing :
∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsTrichotomous α r]
[inst : IsIrrefl β s] (f : α → β), (∀ {x y : α}, r x y → s (f x) (f y)) → Function.Injective f
The theorem states that for any types `α` and `β`, given a relation `r` on `α` and a relation `s` on `β`, if `α` is trichotomous under `r` and `β` is irreflexive under `s`, then any function `f` from `α` to `β` that preserves the order of `α` under `r` (i.e., if `x` is related to `y` under `r` then `f(x)` is related to `f(y)` under `s`), is injective. In other words, an increasing function is injective.
In more mathematical terms, if `f : α → β` is such that whenever `r x y` holds then `s (f x) (f y)` also holds, where `r` is a trichotomous relation on `α` and `s` is an irreflexive relation on `β`, then `f` is injective: for all `a₁, a₂` in `α`, if `f a₁ = f a₂`, then `a₁ = a₂`.
More concisely: If `α` is a trichotomous type and `β` is an irreflexive relation on a type, then any function `f : α → β` preserving the order under `r` is injective.
|
RelEmbedding.isWellFounded
theorem RelEmbedding.isWellFounded :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsWellFounded β s], IsWellFounded α r
This theorem states that if there exists a relation-embedding from a relation 'r' on type 'α' to a relation 's' on type 'β', then, if 's' on 'β' is well-founded, we can conclude that 'r' on 'α' is also well-founded. In other words, the well-foundedness of a relation is preserved under relation-embedding. The term "well-founded" here refers to the property of a relation where no infinite descending chains exist.
More concisely: If there is an embedding of relation r on type α into a well-founded relation s on type β, then r is also well-founded.
|
RelEmbedding.injective
theorem RelEmbedding.injective :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), Function.Injective ⇑f := by
sorry
The theorem `RelEmbedding.injective` states that for any two types `α` and `β`, along with two corresponding relations `r` and `s`, if a function `f` is a relational embedding from `r` to `s`, then `f` is injective. In other words, whenever two elements `x` and `y` of type `α` satisfy `f(x) = f(y)`, it implies `x = y`. This theorem is an important property of relational embeddings in the context of relation-preserving functions.
More concisely: If `f` is a relational embedding from relation `r` on type `α` to relation `s` on type `β`, then `f` is an injective function.
|
RelEmbedding.isWellOrder
theorem RelEmbedding.isWellOrder :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsWellOrder β s], IsWellOrder α r
The theorem `RelEmbedding.isWellOrder` states that for any two types `α` and `β` with relations `r` and `s` respectively, if `r` is embeddable into `s` (denoted by `r ↪r s`), then given `s` is a well-order relation on `β` (captured by `IsWellOrder β s`), it implies `r` is a well-order relation on `α` (represented by `IsWellOrder α r`). In essence, it means that the well-orderedness is preserved under the relative embedding from `r` to `s`.
More concisely: If relation `r` on type `α` is embeddable into relation `s` on type `β` and `s` is a well-order relation on `β`, then `r` is a well-order relation on `α`.
|
RelHomClass.wellFounded
theorem RelHomClass.wellFounded :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
[inst : RelHomClass F r s], F → WellFounded s → WellFounded r
The theorem `RelHomClass.wellFounded` states that for any types `α` and `β`, any binary relations `r` on `α` and `s` on `β`, and any type `F` that behaves like a function from `α` to `β`, if `F` is a relational homomorphism from `r` to `s` (meaning it respects the relations `r` and `s`), then if `s` is a well-founded relation (there are no infinite descending chains), `r` must also be a well-founded relation. In other words, the well-foundedness property is preserved through relational homomorphisms.
More concisely: If `F : α → β` is a function that respects the relational homomorphism between well-founded relations `r` on `α` and `s` on `β`, then `r` is also a well-founded relation.
|
RelEmbedding.isTrans
theorem RelEmbedding.isTrans :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsTrans β s], IsTrans α r
This theorem, `RelEmbedding.isTrans`, states that for any two types `α` and `β`, and any two relations `r` on `α` and `s` on `β`, if `r` is embedded in `s` (`r ↪r s`), and `s` is transitive, then `r` is also transitive. In the context of order theory, this means that the transitivity of an order relation is preserved under order-embedding.
More concisely: If relation `r` on type `α` is embedded in transitive relation `s` on type `β`, then `r` is transitive.
|
RelIso.coe_fn_injective
theorem RelIso.coe_fn_injective :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
The theorem `RelIso.coe_fn_injective` states that for any types `α` and `β`, and any relations `r` on `α` and `s` on `β`, the map that sends a relation-preserving equivalence `f : r ≃r s` (i.e., an isomorphism of relational structures) to its underlying function `⇑f : α → β` is injective. This means that if two such isomorphisms have the same underlying function, then they must be the same isomorphism. This is expressed in Lean with the `Function.Injective` predicate, which asserts that different inputs must give different outputs.
More concisely: Given types `α` and `β`, and relations `r` on `α` and `s` on `β`, the function that maps relation-preserving equivalences `r ≃r s` to their underlying functions is injective.
|
RelIso.rel_symm_apply
theorem RelIso.rel_symm_apply :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : α} {y : β},
r x (e.symm y) ↔ s (e x) y
The theorem `RelIso.rel_symm_apply` asserts that for any two types `α` and `β`, a relation `r` on `α`, a relation `s` on `β`, and a relation isomorphism `e` from `r` to `s`, for any elements `x` of `α` and `y` of `β`, the statement "x is related to the image under the inverse isomorphism of y" in relation `r` is equivalent to the statement "the image under the isomorphism of x is related to y" in relation `s`. This theorem shows the symmetry property of relation isomorphisms.
More concisely: For any relation isomorphisms between relations `r` on type `α` and `s` on type `β`, `x` in `α`, and `y` in `β`, `x` related to `y^(-1) . s(y)` in `r` if and only if `s(x)` is related to `y` in `s`.
|
RelHom.map_rel'
theorem RelHom.map_rel' :
∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
r a b → s (self.toFun a) (self.toFun b)
This theorem states that for any two types `α` and `β`, a relation `r` on `α` and a relation `s` on `β`, and a `RelHom` (relation-preserving function) from `r` to `s`, if the elements `a` and `b` from `α` are related by `r`, then their images under the `RelHom` function are related by `s`. In simpler terms, this theorem asserts that a `RelHom` preserves the relational structure from one set to another.
More concisely: For any relations $r$ on type $\alpha$ and $s$ on type $\beta$, and a RelHom $f$ from $r$ to $s$, if $a$ is related to $b$ by $r$, then $f(a)$ is related to $f(b)$ by $s$.
|
RelIso.ext
theorem RelIso.ext :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄,
(∀ (x : α), f x = g x) → f = g
This theorem states that for any two types `α` and `β`, any relations `r` on `α` and `s` on `β`, and any two relation-preserving isomorphisms `f` and `g` from `r` to `s`, if for every element `x` of type `α`, `f(x)` is equal to `g(x)`, then `f` is equal to `g`. In other words, if two relation-preserving isomorphisms between the same pairs of relations agree on every input, then they are the same isomorphism.
More concisely: If two relation-preserving isomorphisms between the same pairs of relations agree on every input, then they are equal.
|
RelEmbedding.acc
theorem RelEmbedding.acc :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α), Acc s (f a) → Acc r a
This theorem states that for any two types `α` and `β`, and any two binary relations `r` on `α` and `s` on `β`, if there exists a relation-preserving embedding `f` from `r` to `s` (represented as `r ↪r s`), then for any element `a` of type `α`, if `Acc s (f a)` is true (which means that every chain in `s` starting from `f a` is finite), then `Acc r a` is also true (which means every chain in `r` starting from `a` is also finite). The theorem thus establishes a condition under which the accessibility property can be transferred from a relation to its image under a relation-preserving embedding.
More concisely: If there exists a relation-preserving embedding from binary relation `r` on type `α` to binary relation `s` on type `β`, and every chain in `s` starting from the image of an element `a` in `α` is finite, then every chain in `r` starting from `a` is also finite.
|
WellFounded.of_quotient_lift₂
theorem WellFounded.of_quotient_lift₂ :
∀ {α : Type u_1} [inst : Setoid α] {r : α → α → Prop}
{H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
WellFounded (Quotient.lift₂ r H) → WellFounded r
This theorem, referred to as the "Alias of the forward direction of `wellFounded_lift₂_iff`," states that for any type `α` equipped with a Setoid relation, a specific relation `r` is well-founded if its lift to a quotient is well-founded. More specifically, it states that given any four elements of the type `α` (say `a₁`, `b₁`, `a₂`, `b₂`), if `a₁` is equivalent to `a₂` and `b₁` is equivalent to `b₂` under the Setoid equivalence, and this implies that `r a₁ b₁` equals `r a₂ b₂`, then if the lifted relation `Quotient.lift₂ r H` is well-founded, the original relation `r` must also be well-founded. Here, "well-founded" means that there are no infinite descending chains, which is a crucial property in many areas of mathematics, including the study of ordinals and computer science.
More concisely: If a Setoid relation's lifted relation to a quotient is well-founded, then the original relation is also well-founded, given that equivalent elements have equivalent images under the relation.
|
wellFounded_lift₂_iff
theorem wellFounded_lift₂_iff :
∀ {α : Type u_1} [inst : Setoid α] {r : α → α → Prop}
{H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
The theorem `wellFounded_lift₂_iff` states that, for all types `α` that have a setoid structure and for all binary relations `r` on `α`, the relation `r` is well-founded if and only if the relation `r` lifted to the quotient of `α` by this setoid relation is well-founded. This lifted relation is defined by the function `Quotient.lift₂`. Here, well-foundedness of a relation `r` means that there are no infinite descending chains in `r`, and equality of relations is defined by the setoid structure.
More concisely: For any setoid type `α` and binary relation `r` on `α`, `r` is well-founded if and only if the relation `Quotient.lift₂ r` obtained by lifting `r` to the quotient of `α` by the setoid relation is well-founded.
|
RelIso.map_rel_iff
theorem RelIso.map_rel_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a b : α},
s (f a) (f b) ↔ r a b
This theorem states that for all types `α` and `β`, and for all relations `r` on `α` and `s` on `β`, if there is a relative isomorphism `f` from `r` to `s`, then for any two elements `a` and `b` of `α`, `s` holds between `f(a)` and `f(b)` if and only if `r` holds between `a` and `b`. In other words, the relative isomorphism `f` preserves the relational structure between `α` and `β`.
More concisely: Given types `α` and `β`, relations `r` on `α` and `s` on `β`, and a relative isomorphism `f` from `r` to `s`, for all `a, b ∈ α`, `r(a, b)` if and only if `s(f(a), f(b))`.
|
RelHomClass.map_rel
theorem RelHomClass.map_rel :
∀ {F : Type u_5} {α : Type u_6} {β : Type u_7} {r : outParam (α → α → Prop)} {s : outParam (β → β → Prop)}
[inst : FunLike F α β] [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (f a) (f b)
The theorem `RelHomClass.map_rel` states that for any types `F`, `α`, `β`, a relation `r` on `α` and a relation `s` on `β`, if `F` is a function-like structure from `α` to `β` and `F` is also a `RelHomClass` with respect to `r` and `s`, then for any element `f` of type `F` and any elements `a` and `b` of type `α`, if `a` is related to `b` by the relation `r`, then `f(a)` is related to `f(b)` by the relation `s`. In other words, a `RelHomClass` preserves the relation when mapping from `α` to `β`. This is a property that is required in many mathematical structures such as group homomorphisms, linear transformations, etc.
More concisely: Given a function-like structure `F` between types `α` and `β` that is a `RelHomClass` with respect to relations `r` on `α` and `s` on `β`, if `a` and `b` are related by `r`, then `F(a)` is related to `F(b)` by `s`.
|
RelEmbedding.map_rel_iff'
theorem RelEmbedding.map_rel_iff' :
∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
This theorem states that for any two elements `a` and `b` of a certain type `α`, and a relation `r` on `α`, if we have a relation embedding (`RelEmbedding`) from `r` into a relation `s` on another type `β`, then `a` and `b` are related under `s` (after applying the relation embedding) if and only if they are related under `r`. Essentially, the relation `s` on the embedded elements mirrors the relation `r` on the original elements.
More concisely: For any relations `r` on type `α` and `s` on type `β`, and given a relation embedding from `r` to `s`, elements `a` and `b` of `α` are related by `r` if and only if their images under the embedding are related by `s`.
|
RelHom.coe_fn_injective
theorem RelHom.coe_fn_injective :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
The theorem `RelHom.coe_fn_injective` states that for any types `α` and `β` and any relation `r` on `α` and `s` on `β`, the function `coe_fn : (r →r s) → (α → β)` which maps a relation homomorphism to its underlying function is injective. In other words, if two relation homomorphisms from `r` to `s` have the same underlying function, then they must be the same relation homomorphism.
More concisely: If two relation homomorphisms from `r` to `s` have the same underlying function, then they are equal as relation homomorphisms.
|
RelHom.map_rel
theorem RelHom.map_rel :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α},
r a b → s (f a) (f b)
This theorem states that for any types `α` and `β`, and any relations `r` on `α` and `s` on `β`, if `f` is a relation-homomorphism from `r` to `s`, then for any elements `a` and `b` of `α`, if `r a b` holds, then `s (f a) (f b)` also holds. In more plain terms, if `a` is related to `b` under the relation `r`, then the images of `a` and `b` under the relation-homomorphism `f` are related under the relation `s`.
More concisely: If `f` is a relation homomorphism from `r` to `s`, then for all `a, b` in `α`, `r a b` implies `s (f a) (f b)`.
|
acc_lift₂_iff
theorem acc_lift₂_iff :
∀ {α : Type u_1} [inst : Setoid α] {r : α → α → Prop}
{H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a : α},
Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a
The theorem `acc_lift₂_iff` states that for any type `α` with a setoid structure, and for any binary relation `r` on `α`, if `r` respects the equivalence relation of the setoid in the sense that whenever `a₁` is equivalent to `a₂` and `b₁` is equivalent to `b₂`, `r a₁ b₁` equals `r a₂ b₂`, then for any element `a` in `α`, `a` is accessible under the relation `r` if and only if the equivalence class of `a` under the setoid's equivalence relation is accessible under the relation lifted to the quotient by `Quotient.lift₂`. Here, a value is said to be accessible under a relation if there is no infinite descending chain starting from that value.
More concisely: For any setoid type `α` and binary relation `r` respecting its equivalence relation, an element `a` is accessible under `r` if and only if its equivalence class is accessible under the relation lifted to the quotient.
|
WellFounded.quotient_liftOn₂'
theorem WellFounded.quotient_liftOn₂' :
∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop}
{H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → r a₁ a₂ = r b₁ b₂},
WellFounded r → WellFounded fun x y => x.liftOn₂' y r H
This theorem states that for any type `α`, an equivalence relation `s` on `α`, and a relation `r` on `α` that respects the equivalence relation (i.e., for any `a₁`, `a₂`, `b₁`, `b₂` of `α`, if `a₁` is equivalent to `b₁` and `a₂` is equivalent to `b₂` under `s`, then `r` holds between `a₁` and `a₂` if and only if it holds between `b₁` and `b₂`), if `r` is well-founded (i.e., there are no infinite descending chains), then the relation defined by taking the quotient of `α` by `s` and applying `r` is also well-founded. In other words, the well-foundedness of `r` is preserved under the quotienting process.
More concisely: If `α` is a type, `s` is an equivalence relation on `α`, `r` is a well-founded relation on `α` respecting `s`, then the relation `r` on the quotient `α / s` is also well-founded.
|
RelEmbedding.coe_toEmbedding
theorem RelEmbedding.coe_toEmbedding :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s}, ⇑f.toEmbedding = ⇑f
This theorem states that for any two types `α` and `β`, and for any two relations `r` and `s` on `α` and `β` respectively, and for any relational embedding `f` from `r` to `s`, the function obtained by applying the `toEmbedding` method to `f` is equal to `f`. In other words, converting a relationally-embedded function to an embedding does not change its behavior.
More concisely: For any relations $r$ on type $\alpha$, $s$ on type $\beta$, and relational embedding $f$ from $r$ to $s$, the function obtained by applying `toEmbedding` method to $f$ equals $f$.
|
RelHom.ext
theorem RelHom.ext :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r →r s⦄,
(∀ (x : α), f x = g x) → f = g
This theorem, `RelHom.ext`, states that for any types `α` and `β`, any relations `r` on `α` and `s` on `β`, and any two relation-preserving functions `f` and `g` from `α` to `β` satisfying `r` and `s` respectively, if for every `α` the results of `f` and `g` are equal, then `f` and `g` are identical. Essentially, this is a statement of extensionality for relation-preserving functions: two such functions are equal if they agree on all inputs.
More concisely: If two relation-preserving functions between types agree on every input with respect to given relations, then they are equal.
|
RelIso.symm_apply_apply
theorem RelIso.symm_apply_apply :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : α), e.symm (e x) = x := by
sorry
The theorem `RelIso.symm_apply_apply` states that for any types `α` and `β`, any relations `r` and `s` on `α` and `β` respectively, any relation isomorphism `e` between `r` and `s`, and any element `x` of type `α`, applying the inverse (or symmetry) of the isomorphism `e` to the result of applying `e` to `x` yields back the original element `x`. In other words, the inverse operation of a relation isomorphism undoes the effect of the original operation.
More concisely: For any relation isomorphisms between types and relations, application of the inverse isomorphism to the composition of the original isomorphism with an element maps the element back to its original value.
|
Function.Surjective.wellFounded_iff
theorem Function.Surjective.wellFounded_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α → β},
Function.Surjective f → (∀ {a b : α}, r a b ↔ s (f a) (f b)) → (WellFounded r ↔ WellFounded s)
The theorem `Function.Surjective.wellFounded_iff` states that for any types `α` and `β`, any relations `r` on `α` and `s` on `β`, and any function `f` from `α` to `β` which is surjective, if the relation `r` between any two elements `a` and `b` of `α` equates to the relation `s` between `f(a)` and `f(b)`, then `r` is well-founded if and only if `s` is well-founded. In terms of mathematics, this theorem is saying that the well-foundedness of a relation is preserved under a surjective function if the relations on the domain and codomain are equivalent under the function.
More concisely: A surjective function preserves the well-foundedness of relations between related elements.
|
RelIso.toEquiv_injective
theorem RelIso.toEquiv_injective :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective RelIso.toEquiv
The theorem `RelIso.toEquiv_injective` states that, for any types `α` and `β`, and any binary relations `r` on `α` and `s` on `β`, the function `RelIso.toEquiv` is injective. In other words, if we have two relations that are isomorphic (denoted as `r ≃r s`), and the isomorphisms are converted to equivalences between the original types using `RelIso.toEquiv`, then distinct isomorphisms will produce distinct equivalences. This means that if two equivalences are equal, they must have originated from the same relational isomorphism.
More concisely: If two binary relations `r` and `s` on types `α` and `β` are isomorphic, then the corresponding equivalences `RelIso.toEquiv r` and `RelIso.toEquiv s` are equal.
|