biUnion_filter_atomise — Mathlib

English

Given t ∈ F with t ⊆ s, the union of all nonempty blocks contained in t from the atomised partition equals t.

Русский

Пусть t ∈ F и t ⊆ s; объединение всех непустых блоков разбиения atomise(s,F), лежащих внутри t, равно t.

LaTeX

$$$\\bigcup\\{u\\in (atomise(s,F)).parts : u\\subseteq t, u\\neq \\emptyset\\} = t$$$

Lean4

theorem biUnion_filter_atomise (ht : t ∈ F) (hts : t ⊆ s) :
    {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t :=
  by
  ext a
  refine mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩
  obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)
  refine ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩
  obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2
  rw [mem_filter] at hau hb
  rwa [← hb.2 _ ht, hau.2 _ ht]

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