sInf_within_of_ordConnected
theorem sInf_within_of_ordConnected :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set ↑s⦄,
t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
The theorem `sInf_within_of_ordConnected` states that for any type `α` which has a conditionally complete linear order structure, given any Order-Connected set `s` of this type, for all nonempty subsets `t` of `s` that are bounded below, the greatest lower bound (infimum) of the elements of `t` when projected back to the underlying type `α` via the subtype `val` function, is still an element of the original set `s`.
More concisely: For any order-connected subset `s` of a conditionally complete linearly ordered type `α`, the infimum of any nonempty bounded-below subset `t` of `s` lies in `s`.
|
subset_sInf_of_within
theorem subset_sInf_of_within :
∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : InfSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s → sInf (Subtype.val '' t) = ↑(sInf t)
This theorem, `subset_sInf_of_within`, states that for any type `α`, given a set `s` of this type with a preorder and an inhabited subtype, and another set `t` which is a subset of the subtype of `s`, if `t` is nonempty and bounded below, and if the greatest lower bound (infimum or `sInf`) of the image of `t` under the `Subtype.val` function is an element of `s`, then this greatest lower bound is equal to the infimum of `t` coerced into the base type. In other words, the theorem asserts that within a certain subset of a type, if conditions of non-emptiness, lower bound, and inhabitation are met, infimums in the subset and the larger set coincide.
More concisely: If `s` is a non-empty subset of a type `α` with a preorder and an inhabited subtype, and `t` is a bounded below subset of `s`, such that the infimum of `t` in the subtype exists and is an element of `s`, then the infimum of `t` in the subtype equals the infimum of `t` coerced into the base type.
|
sSup_within_of_ordConnected
theorem sSup_within_of_ordConnected :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set ↑s⦄,
t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
The theorem `sSup_within_of_ordConnected` states that for any type `α` with a conditionally complete linear order, any ordered and connected set `s` of type `α`, and any subset `t` of the elements in `s` (represented as subtypes), if `t` is nonempty and has an upper bound, then the supremum (least upper bound) of the values contained in `t` belongs to the set `s`. In other words, this theorem ensures that the supremum of any nonempty, bounded-above subset of an ordered and connected set lies within the set itself.
More concisely: If `α` is a type with a conditionally complete linear order, `s` is an ordered and connected subset of `α` with a nonempty, bounded-above subset `t`, then the supremum of `t` belongs to `s`.
|
subset_sSup_of_within
theorem subset_sSup_of_within :
∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s → sSup (Subtype.val '' t) = ↑(sSup t)
The theorem `subset_sSup_of_within` states that for any type `α` with a preorder and a superset structure, and for any set `s` of type `α` that has an inhabitant, if we have a subset `t` of `s` that is nonempty and is bounded by an upper bound, then if the supremum of the image of `t` under the subtype value function is an element of `s`, it equals the coerced supremum of `t`. This essentially says that if we restrict ourselves to a subset of a bounded set, the supremum of the subset is the same as the supremum of the set when viewed in the larger context.
More concisely: If `s` is a nonempty, bounded subset of a preordered type `α` with a supremum, and the supremum of `s` is an element of `s`, then the supremum of `s` equals the coerced supremum of `s`.
|