Finset.ordConnected_range_val
theorem Finset.ordConnected_range_val : ∀ {α : Type u_1}, (Set.range Finset.val).OrdConnected
The theorem `Finset.ordConnected_range_val` states that for any type `α`, the Finsets of that type form an order-connected suborder of multisets. In other words, for any two elements in the range of the `Finset.val` function, all elements that lie in between these two in the order are also included in the range of `Finset.val`. This basically means that there are no 'gaps' in the ordering of elements in the range of `Finset.val`, establishing it as an order-connected subset of multisets.
More concisely: For any type `α`, the range of the `Finset.val` function on `Finset α` forms an order-connected subset of multisets over `α`.
|
Finset.ordConnected_range_coe
theorem Finset.ordConnected_range_coe : ∀ {α : Type u_1}, (Set.range Finset.toSet).OrdConnected
This theorem asserts that for any given type `α`, the range of the function `Finset.toSet` forms an order-connected suborder of sets. In other words, for any two elements in the set created from a `Finset`, every element that is in-between these two elements (according to the order defined on `α`) is also included in the set. This property is captured by the term `Set.OrdConnected` in Lean. Essentially, it means that finite sets (represented as `Finset` in Lean) preserve the order connectivity when they are converted to sets in Lean (`Set α`).
More concisely: For any type `α` and `Finset` `s` of elements from `α`, the image of `s` under the function `Finset.toSet` forms an order-connected subset of the power set `Set α`.
|
WCovBy.finset_coe
theorem WCovBy.finset_coe : ∀ {α : Type u_1} {s t : Finset α}, s ⩿ t → ↑s ⩿ ↑t
This theorem, `WCovBy.finset_coe`, states that for any types `α` and any finite sets `s` and `t` of type `α`, if `s` is weakly covered by `t` (denoted as `s ⩿ t`), then the set of elements of `s` (denoted as `↑s`) is also weakly covered by the set of elements of `t` (denoted as `↑t`). This theorem is an alias of the reverse direction of the theorem `Finset.coe_wcovBy_coe`.
More concisely: If a finite set `s` is weakly covered by another finite set `t`, then the elements of `s` are weakly covered by the elements of `t`.
|
CovBy.finset_coe
theorem CovBy.finset_coe : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → ↑s ⋖ ↑t
This theorem, `CovBy.finset_coe`, is an alias of the reverse direction of `Finset.coe_covBy_coe`. In plain language, it states that for all types `α` and for all finite sets `s` and `t` of type `α`, if `s` is covered by `t` (denoted as `s ⋖ t`), then the set of elements of `s` (denoted as `↑s`) is also covered by the set of elements of `t` (denoted as `↑t`).
More concisely: If `s` is a subset of `t` and `s` is finite, then the image of `s` under the covariant functor `↑` (which maps finite sets to their underlying sets) is a subset of the image of `t` under `↑`.
|
Mathlib.Data.Finset.Grade._auxLemma.16
theorem Mathlib.Data.Finset.Grade._auxLemma.16 : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ = s₂) = (↑s₁ = ↑s₂) := by
sorry
This theorem, named `Mathlib.Data.Finset.Grade._auxLemma.16`, states that for any type `α` and any two finite sets `s₁` and `s₂` of type `α`, `s₁` is equal to `s₂` if and only if the coercions of `s₁` and `s₂` to sets are equal. This is essentially saying that two finite sets are equal if their underlying set representations are equal.
More concisely: Two finite sets of type `α` are equal if and only if their underlying set representations are equal.
|
WCovBy.finset_val
theorem WCovBy.finset_val : ∀ {α : Type u_1} {s t : Finset α}, s ⩿ t → s.val ⩿ t.val
This theorem, `WCovBy.finset_val`, states that for any two finite sets `s` and `t` of an arbitrary type `α`, if `s` weakly covers `t` (denoted as `s ⩿ t`), then the underlying list of elements (or the "value") of `s` weakly covers the underlying list of elements of `t`. In other words, the 'weak cover' relationship is preserved when we consider the lists of elements in the finite sets `s` and `t`, instead of the sets themselves.
More concisely: If two finite sets `s` and `t` of type `α` weakly cover each other, then their underlying lists of elements have the same elements (up to multiset equality).
|
CovBy.finset_val
theorem CovBy.finset_val : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → s.val ⋖ t.val
This theorem, referred to as `CovBy.finset_val`, states that for any two finite sets `s` and `t` of any type `α`, if `s` is covered by `t` then the value set of `s` is also covered by the value set of `t`. This theorem represents the reverse direction of the theorem `Finset.val_covBy_val`. In the context of this theorem, 'covered by' is represented by the `⋖` symbol.
More concisely: If `s ⋖ t`, then `set.val s ⊆ set.val t` for any finite sets `s` and `t` of type `α`.
|