Finset.card_sigmaLift
theorem Finset.card_sigmaLift :
∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
(f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : (i : ι) × α i) (b : (i : ι) × β i),
(Finset.sigmaLift f a b).card = if h : a.fst = b.fst then (f (h ▸ a.snd) b.snd).card else 0
The theorem `Finset.card_sigmaLift` states that for any types `ι`, `α`, `β`, `γ`, where `α`, `β`, `γ` are dependent on `ι`, and a function `f` that maps each element `i` of type `ι` with a pair of elements `α i` and `β i` to a finite set of `γ i`, and a pair of elements `a` and `b` formed by an element of `ι` and an element of `α i` and `β i` respectively, the cardinality of the finite set obtained by lifting the function `f` to the pair `a` and `b` is equal to the cardinality of the finite set obtained by applying `f` to the second elements of the pair `a` and `b` if the first elements of `a` and `b` are equal, otherwise it is 0.
More concisely: For any function `f` mapping elements of type `ι` to finite sets of `γ` indexed by `α` and `β` dependent on `ι`, the cardinality of `f` applied to `(a, b)` where `a` and `b` have equal first components equals the cardinality of `f` applied to `b`, otherwise it is 0.
|
biSup_finsetSigma
theorem biSup_finsetSigma :
∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset ι)
(t : (i : ι) → Finset (α i)) (f : Sigma α → β), ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
The theorem `biSup_finsetSigma` states that, for any types `ι`, function `α` from `ι` to any type, and type `β` which is a complete lattice, given a finite set `s` of type `ι`, a function `t` from `ι` to a finite set of `α i`, and a function `f` from the sigma type of `α` to `β`, the supremum of `f` over the dependent pairs `⟨i, a⟩` in the sigma finite set of `s` and `t` is equal to the double supremum first over `i` in `s` and then over `j` in `t i` of `f` applied to the pair `⟨i, j⟩`. In other words, this theorem states the equality between a single supremum over a joint set and a sequential pair of suprema over the individual sets.
More concisely: For any complete lattice β, finite set s of type ι, function t from ι to finite sets of α, and function f from the sigma type of α over s and t to β, the supremum of f over the dependent pairs ⟨i, a⟩ in the sigma finite set of s and t is equal to the double supremum of f first over i in s and then over j in ti.
|
Finset.mem_sigmaLift
theorem Finset.mem_sigmaLift :
∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
(f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ),
x ∈ Finset.sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
The theorem `Finset.mem_sigmaLift` asserts that for any types `ι`, `α i`, `β i` and `γ i` where `i` ranges over `ι` and there is a decidable equality on `ι`, and for any function `f` that maps pairs of elements from `α i` and `β i` to a finite set of `γ i`, an element `x` from `Sigma γ` (a dependent pair type where the first component is from `ι` and the second component is from `γ i`) belongs to the finite set produced by `Finset.sigmaLift f` applied to a pair of elements from `Sigma α` and `Sigma β`, if and only if there exist proofs `ha` and `hb` that the first component of `a` and `b` respectively (which are both from `ι`) equal the first component of `x`, and the second component of `x` belongs to the finite set produced by the function `f` applied to the second components of `a` and `b` (which are from `α i` and `β i` respectively) under the equality assumptions `ha` and `hb`.
More concisely: For any decidably equipped types `ι`, `α i`, `β i`, and `γ i`, and decidable equality `=_`, if `f : Π i, α i × β i → Finset γ i`, then `x ∈ Finset.sigmaLift f (a, b)` if and only if there exist `ha : a = a'_i`, `hb : b = b'_i`, and `y ∈ f (a'_i, b'_i)` such that `x = (i, y)`.
|
Mathlib.Data.Finset.Sigma._auxLemma.1
theorem Mathlib.Data.Finset.Sigma._auxLemma.1 :
∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i},
(a ∈ s.sigma t) = (a.fst ∈ s ∧ a.snd ∈ t a.fst)
The theorem `Mathlib.Data.Finset.Sigma._auxLemma.1` states that for any types `ι` and `α` (which is a function from `ι` to some type), any finite set `s` of type `ι`, any function `t` from `ι` to a finite set of `α i`, and any dependent pair `a` of type `ι` and `α i`, the pair `a` belongs to the set `s.sigma t` if and only if the first element of `a` belongs to `s` and the second element of `a` belongs to the set `t` at the index of the first element of `a`.
In mathematical terms, if `a` is the pair `(i, a_i)` where `i` belongs to `s` and `a_i` belongs to the `t(i)`, then `a` belongs to the finite set `σ` of all such pairs generated by `s` and `t`.
More concisely: For any type `ι`, function `t` from `ι` to finite sets of type `α i`, finite set `s` of type `ι`, and pairs `(i, a\_i)` of type `ι × α i`, `(i, a\_i)` is in the set `s.sigma t` if and only if `i` is in `s` and `a\_i` is in `t i`.
|
Finset.mem_sigma
theorem Finset.mem_sigma :
∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i},
a ∈ s.sigma t ↔ a.fst ∈ s ∧ a.snd ∈ t a.fst
The theorem `Finset.mem_sigma` states that for all types `ι` and `α`, where `α` is a type dependent on `ι`, a given finset `s` of `ι`, a function `t` that takes an element of `ι` and returns a finset of `α i`, and a dependent pair `a` of type `ι` and `α i`, `a` is an element of the finset `sigma s t` if and only if the first component of `a` is in `s`, and its second component is in the finset `t` applied to the first component of `a`. In mathematical terms, this theorem says that a dependent pair belongs to the Cartesian product of a set and a family of sets indexed by that set exactly when its first component belongs to the set and its second component belongs to the particular set in the family indexed by the first component.
More concisely: For all types `ι` and `α`, and for every finset `s` of `ι`, function `t : ι → Finset α`, and dependent pair `a : ι × α`, `a` is in the image of `σ` (the finite sum) of `s` and `t`, if and only if the first component of `a` is in `s` and the second component is in `t` applied to the first component of `a`.
|