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]