iInf_principal — Mathlib

English

If a finite set t of indices has pairwise disjoint l_i, then there exist sets s_i ∈ l_i forming a pairwise disjoint family.

Русский

Если конечное множество индексов t имеет попарно несовместные l_i, то существуют множества s_i ∈ l_i, образующие попарно несовместное семейство.

LaTeX

$$$ t.PairwiseDisjoint l \to\ t.Finite \to \exists s: ι \to Set α, (\forall i, s i ∈ l i) ∧ t.PairwiseDisjoint s $$$

Lean4

theorem iInf_principal {ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i) :=
  by
  cases nonempty_fintype (PLift ι)
  rw [← iInf_plift_down, ← iInter_plift_down]
  simpa using iInf_principal_finset Finset.univ (f <| PLift.down ·)

Похожие утверждения