sUnion_memPartition — Mathlib

English

The union of all blocks in memPartition(f,n) covers the whole space.

Русский

Объединение всех блоков memPartition(f,n) покрывает всё пространство.

LaTeX

$$$\\bigcup \\operatorname{memPartition}(f,n) = \\operatorname{univ}$$$

Lean4

@[simp]
theorem sUnion_memPartition (f : ℕ → Set α) (n : ℕ) : ⋃₀ memPartition f n = univ := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    ext x
    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
    simp only [mem_sUnion, mem_univ, iff_true] at this ⊢
    obtain ⟨t, ht, hxt⟩ := this
    by_cases hxf : x ∈ f n
    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩

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