English
For a fixed t ∈ F, the number of nonempty blocks of atomise(s,F) contained in t is at most 2^{|F|-1}.
Русский
Для фиксированного t ∈ F число непустых блоков atomise(s,F) внутри t не превосходит 2^{|F|-1}.
LaTeX
$$$\\#\\{u\\in (atomise(s,F)).parts : u\\subseteq t, u\\neq \\emptyset\\} \\le 2^{(|F|-1)}$$$
Lean4
theorem card_filter_atomise_le_two_pow (ht : t ∈ F) :
#({u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}) ≤ 2 ^ (#F - 1) :=
by
suffices h :
{u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
(F.erase t).powerset.image fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}
by
refine (card_le_card h).trans (card_image_le.trans ?_)
rw [card_powerset, card_erase_of_mem ht]
rw [subset_iff]
simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise, and_imp,
Finset.Nonempty, exists_imp, and_imp]
rintro P' i hi P PQ rfl hy₂ j _hj
refine ⟨P.erase t, erase_subset_erase _ PQ, ?_⟩
simp only [insert_erase (((mem_filter.1 hi).2 _ ht).2 <| hy₂ hi)]
