biSup_sigma
theorem biSup_sigma :
∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} [inst : CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i))
(f : Sigma α → β), ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
The `biSup_sigma` theorem states that for any types `ι`, `α` (which is indexed by `ι`), and `β` (which is a complete lattice), any set `s` of type `ι`, any indexed set `t` of type `α`, and any function `f` from the sigma type `Sigma α` to `β`, the supremum (notated as `⨆`) of `f ij` for `ij` in the indexed sum of sets `Set.sigma s t` is equal to the supremum of `f` applied to the pair `{ fst := i, snd := j }` for `i` in `s` and `j` in `t i`. In other words, this is saying that applying the function `f` to each element in the indexed sum of sets and taking the supremum gives the same result as first taking the supremum over each set individually and then taking the overall supremum.
More concisely: For any complete lattice β, type ι, type α indexed by ι, set s of ι, indexed set t of α over s, and function f from the sigma type Sigma α to β, the supremum of f applied to each pair (i, j) in Set.sigma s t is equal to the supremum of the images f(i, j) over i in s and the supremum of the images over j in t i.
|
Mathlib.Data.Set.Sigma._auxLemma.2
theorem Mathlib.Data.Set.Sigma._auxLemma.2 :
∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {x : (i : ι) × α i},
(x ∈ s.sigma t) = (x.fst ∈ s ∧ x.snd ∈ t x.fst)
This theorem states that for any index set `ι`, any function `α` from `ι` to some type, any set `s` of type `ι`, any function `t` from `ι` to a set of elements of type `α i`, and any dependent pair `x` consisting of an element of `ι` and an element of type `α i`, `x` is a member of the indexed sum of sets `s.sigma t` if and only if the first component of `x` is a member of `s` and the second component of `x` is a member of `t` corresponding to the first component of `x`. In other words, it specifies the membership criteria for the indexed sum of sets (also known as Sigma set) in terms of the original sets and their indexing.
More concisely: For any index set `ι`, set `s` and function `t` from `ι` to sets, an element `(i, x)` is in the indexed sum `s.sigma t` if and only if `i` is in `s` and `x` is in `t i`.
|