English
Definition constructing a filter with cardinal c-intersection property from a base family l, with hl and h_mono guiding the univ and subset-closure structure.
Русский
Определение конструирует фильтр с свойством пересечения по кардиналу c из базовой семьи l, управляемой hl и h_mono через единство и замыкание по подмножествам.
LaTeX
$$$\\text{Definition of } \\mathrm{CardinalInterFilter} \\text{ from } l, c, hl, h_mono$$$
Lean4
/-- Construct a filter with cardinal `c` intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the cardinal `c` intersection property. -/
def ofCardinalInter (l : Set (Set α)) (hc : 2 < c) (hl : ∀ S : Set (Set α), (#S < c) → S ⊆ l → ⋂₀ S ∈ l)
(h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α
where
sets := l
univ_sets := sInter_empty ▸ hl ∅ (mk_eq_zero (∅ : Set (Set α)) ▸ lt_trans zero_lt_two hc) (empty_subset _)
sets_of_superset := h_mono _ _
inter_sets {s t} hs
ht :=
sInter_pair s t ▸ by
apply hl _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
have : #({ s, t } : Set (Set α)) ≤ 2 := by
calc
_ ≤ #({ t } : Set (Set α)) + 1 := Cardinal.mk_insert_le
_ = 2 := by norm_num
exact lt_of_le_of_lt this hc
