InitialSeg.init'
theorem InitialSeg.init' :
∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : r ≼i s) (a : α) (b : β),
s b (self.toRelEmbedding a) → ∃ a', self.toRelEmbedding a' = b
This theorem states that for any two types `α` and `β`, and any two binary relations `r` on `α` and `s` on `β`, if `r` is an order embedding of `s` (denoted as `r ≼i s`), then for any elements `a` in `α` and `b` in `β`, if `s` relates `b` to the image of `a` under the order embedding, there exists an `a'` in `α` such that the image of `a'` under the order embedding equals `b`. This essentially means that the order embedding is an initial segment: any element in `β` that is related to an element in the image of `α` is itself in the image of `α`.
More concisely: Given order embeddings `r: α → β` of relations `r` on type `α` and `s` on type `β`, if `r ≼i s`, then for all `a ∈ α` and `b ∈ β` with `s b = r(a')` for some `a' ∈ α`, there exists `a ∈ α` such that `r a = b`.
|
PrincipalSeg.down
theorem PrincipalSeg.down :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
s b f.top ↔ ∃ a, f.toRelEmbedding a = b
This theorem, `PrincipalSeg.down`, states that for all types `α` and `β`, and for all relations `r` and `s` on these types respectively, if `f` is a principal segment of `s` with respect to `r`, then for any element `b` of `β`, `b` is related to the `top` of `f` under `s` if and only if there exists an element `a` in `α` such that `a` is mapped to `b` by the relation embedding of `f`. Essentially, it's a way of expressing the properties of a principal segment in terms of an existential property on its relation embedding.
More concisely: For any types `α` and `β`, relations `r` on `α` and `s` on `β`, and principal segment `f` of `s` with respect to `r`, an element `b` of `β` is related to the top of `f` under `s` if and only if there exists an element `a` in `α` such that `a` is related to `b` under the relation embedding of `f` and `r`.
|
InitialSeg.init
theorem InitialSeg.init :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
s b (f a) → ∃ a', f a' = b
This theorem states that for all types `α` and `β` with relations `r` and `s` respectively, given that the relation `r` is an initial segment of `s` under a function `f`, then for any elements `a` from `α` and `b` from `β`, if `s` relates `b` to the image of `a` under `f`, there exists an element `a'` in `α` such that `f` maps `a'` to `b`. In other words, if `b` follows `f(a)` in the `s` relation, `b` is also the image of some element in `α` under `f`.
More concisely: Given relations `r` on type `α` and `s` on type `β`, if `r` is an initial segment of `s` under a function `f` and `s(b) ∋ f(a)`, then there exists `a' ∈ α` such that `f(a') = b`.
|
PrincipalSeg.down'
theorem PrincipalSeg.down' :
∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : r ≺i s) (b : β),
s b self.top ↔ ∃ a, self.toRelEmbedding a = b
This theorem, `PrincipalSeg.down'`, asserts that for any types `α` and `β`, relations `r` and `s`, and an order-embedding `self` from `r` into `s`, and any element `b` in `β`, `s b self.top` is true if and only if there exists an element `a` in `α` such that the order-embedding of `a` is equal to `b`. This effectively says that the image of the order embedding is the set of elements `b` in `β` that are related by `s` to the top element of the embedding.
More concisely: For any order-embeddings `self : r → s` between types `r` and `s`, and relations `r` and `s`, the image of the top element of `self` under `s` is equal to the set of elements in `s` that are related to the top element of `r` by `r`.
|
wellFounded_iff_wellFounded_subrel
theorem wellFounded_iff_wellFounded_subrel :
∀ {β : Type u_4} {s : β → β → Prop} [inst : IsTrans β s],
WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
This theorem states that a relation is well-founded if, and only if, every principal segment of it is well-founded. Here, a principal segment of a relation 's' is a subset of the relation that includes all elements related to a given element 'b'. The theorem applies to a transitive relation 's' on a type 'β'. The principal segments are represented by the `Subrel` function applied to 's' and the set of elements 'b'' such that 's b'' b' holds. A relation is well-founded if it contains no infinite descending chains.
More concisely: A transitive relation on a type is well-founded if and only if every principal segment of the relation is well-founded.
|
PrincipalSeg.init
theorem PrincipalSeg.init :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α}
{b : β}, s b (f.toRelEmbedding a) → ∃ a', f.toRelEmbedding a' = b
This theorem, `PrincipalSeg.init`, states that for any two types `α` and `β`, two relations `r` on α and `s` on β, and a function `f` which is an initial segment of `r` with respect to `s` (`r ≺i s`), if `s` is transitive and there exists an element `b` in `β` such that `s b (f.toRelEmbedding a)`, then there exists an element `a'` in `α` such that the relational embedding of `a'` through `f` equals `b`. In other words, for every `b` in the image of `s` which is greater than the image of `a` under `f`, there must exist an `a'` in `α` which embeds to `b` under `f`.
More concisely: Given types `α` and `β`, relations `r` on `α` and `s` on `β`, and a function `f` such that `r ≺i s` and `s` is transitive, if there exists an element `b` in the image of `s` with `s(b) ⊆ f(r(a))` for some `a` in `α`, then there exists an `a'` in `α` such that `f(a') = b`.
|
PrincipalSeg.lt_top
theorem PrincipalSeg.lt_top :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) (a : α),
s (f.toRelEmbedding a) f.top
This theorem, `PrincipalSeg.lt_top`, states that for all types `α` and `β`, and relations `r` on `α` and `s` on `β`, if we have a principal segment `f` from `r` to `s`, and any element `a` of type `α`, then the relation `s` holds between the image of `a` under the relational embedding of `f` and the top element of `f`. In other words, if `f` is a principal segment from one relation space to another, all elements from the source space are related (via `s`) to the top element of `f` when embedded into the target space.
More concisely: For any types `α` and `β`, relations `r` on `α` and `s` on `β`, and a principal segment `f` from `r` to `s`, for all `a` in `α`, `s(f a)` holds.
|
InitialSeg.eq
theorem InitialSeg.eq :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f g : r ≼i s)
(a : α), f a = g a
This theorem asserts that for any two types `α` and `β` with respective order relations `r` and `s`, and given `β` is a well-order, then for any two initial segment embeddings `f` and `g` from `α` into `β`, these embeddings are identical at every point `a` in `α`. In other words, if `f` and `g` are both initial segment embeddings of `α` into `β`, then they are the same function.
More concisely: If `α` is a type with a well-order `r`, and `f` and `g` are initial segment embeddings of `α` into another well-order `β` with order relation `s`, then `f = g`.
|
InitialSeg.init_iff
theorem InitialSeg.init_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
s b (f a) ↔ ∃ a', f a' = b ∧ r a' a
This theorem, named `InitialSeg.init_iff`, states that for all types `α` and `β`, and for all relations `r` on `α` and `s` on `β`, if there exists an initial segment function `f` from `r` to `s`, then for any `a` in `α` and `b` in `β`, `s b (f a)` is equivalent to the statement that there exists an `a'` in `α` such that `f a'` is equal to `b` and `r a' a` is true. In other words, `b` is related to the image of `a` under `f` in the relation `s` if and only if `b` is the image under `f` of some `a'` that is related to `a` in the relation `r`.
More concisely: For all relations $r$ on type $\alpha$ and $s$ on type $\beta$, and for any function $f$ that is an initial segment from $r$ to $s$, $s(b)(f(a))$ holds if and only if there exists $a'$ such that $f(a') = b$ and $r(a' , a)$ holds.
|
InitialSeg.map_rel_iff
theorem InitialSeg.map_rel_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s),
s (f a) (f b) ↔ r a b
This theorem, `InitialSeg.map_rel_iff`, states that for all types `α` and `β`, and for all relations `r` on `α` and `s` on `β`, and for all elements `a` and `b` of type `α`, if there exists an initial segment `f` from `r` to `s`, then the relation `s` holds between `f(a)` and `f(b)` if and only if the relation `r` holds between `a` and `b`. This essentially says that the initial segment `f` maps the relation `r` onto the relation `s`.
More concisely: Given types `α` and `β`, relations `r` on `α` and `s` on `β`, and elements `a` and `b` of type `α`, if there exists an initial segment `f` from `r` to `s`, then `r(a, b)` if and only if `s(f(a), f(b))`.
|