English
The collection of measurable sets, viewed as a subset of sets, carries a Boolean algebra structure.
Русский
Множество измеримых множеств, рассматриваемое как подмножество множеств, имеет структуру булевой алгебры.
LaTeX
$$$\\text{BooleanAlgebra}(\\mathrm{Subtype}(\\mathrm{MeasurableSet}))$$$
Lean4
/-- Boxes of countably spanning sets are countably spanning. -/
theorem pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
IsCountablySpanning (pi univ '' pi univ C) :=
by
choose s h1s h2s using hC
cases nonempty_encodable (ι → ℕ)
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
refine ⟨fun n => Set.pi univ fun i => s i (e n i), fun n => mem_image_of_mem _ fun i _ => h1s i _, ?_⟩
simp_rw [e, (surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i), iUnion_univ_pi s,
h2s, pi_univ]
