English
A set s belongs to cardinalGenerate g hc if and only if there exists S ⊆ g with |S| < c and ⋂ S ⊆ s.
Русский
Множество s принадлежит cardinalGenerate g hc тогда и только тогда, когда существует S ⊆ g такие, что |S| < c и ⋂ S ⊆ s.
LaTeX
$$$s \in cardinalGenerate(g, hc) \iff \exists S \subseteq g, \lvert S \rvert < c \land \bigcap S \subseteq s$$$
Lean4
/-- A set is in the `cardinalInterFilter` generated by `g` if and only if
it contains an intersection of `c` elements of `g`. -/
theorem mem_cardinaleGenerate_iff {s : Set α} {hreg : c.IsRegular} :
s ∈ cardinalGenerate g (IsRegular.nat_lt hreg 2) ↔ ∃ S : Set (Set α), S ⊆ g ∧ (#S < c) ∧ ⋂₀ S ⊆ s :=
by
constructor <;> intro h
·
induction h with
| @basic s hs =>
refine ⟨{ s }, singleton_subset_iff.mpr hs, ?_⟩
simpa [subset_refl] using IsRegular.nat_lt hreg 1
| univ => exact ⟨∅, ⟨empty_subset g, mk_eq_zero (∅ : Set <| Set α) ▸ IsRegular.nat_lt hreg 0, by simp⟩⟩
| superset _ _ ih => exact Exists.imp (by tauto) ih
| @sInter S Sct _ ih =>
choose T Tg Tct hT using ih
refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
apply subset_sInter
apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
rcases h with ⟨S, Sg, Sct, hS⟩
have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c := cardinalInter_ofCardinalGenerate _ _
exact mem_of_superset ((cardinal_sInter_mem Sct).mpr (fun s H => CardinalGenerateSets.basic (Sg H))) hS
