English
Instance giving CardinalInterFilter for comap f l when l has CardinalInterFilter c.
Русский
Инстанс для CardinalInterFilter фильтра comap f l, если l имеет CardinalInterFilter c.
LaTeX
$$$CardinalInterFilter(\\mathrm{comap}(f, l), c)$$$
Lean4
/-- Construct a filter with cardinal `c` intersection property.
Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
Similarly to `Filter.ofCardinalInter`,
this constructor deduces some properties from the cardinal `c` intersection property
which becomes the cardinal `c` union property because we take complements of all sets. -/
def ofCardinalUnion (l : Set (Set α)) (hc : 2 < c) (hUnion : ∀ S : Set (Set α), (#S < c) → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
(hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α :=
by
refine .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
· rw [mem_setOf_eq, compl_sInter]
apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)
intro s hs
rw [mem_image] at hs
rcases hs with ⟨t, ht, rfl⟩
apply hSp ht
· rw [mem_setOf_eq]
rw [← compl_subset_compl] at hsub
exact hmono sᶜ ht tᶜ hsub
