English
For any l and hc, hunion, hmono, the membership of s in ofCardinalUnion corresponds to membership of its complement in l.
Русский
Для любых l, hc, hunion, hmono выполняется: s ∈ ofCardinalUnion ⇔ s^c ∈ l.
LaTeX
$$$s \\in \\mathrm{ofCardinalUnion}(l, hc hunion hmono) \\iff l s^{\\complement}$$$
Lean4
/-- Infimum of two `CardinalInterFilter`s is a `CardinalInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
instance cardinalInterFilter_inf_eq (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c] :
CardinalInterFilter (l₁ ⊓ l₂) c := by
refine ⟨fun S hSc hS => ?_⟩
choose s hs t ht hst using hS
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (cardinal_bInter_mem hSc).2 hs
replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (cardinal_bInter_mem hSc).2 ht
refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
rw [hst i hi]
apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)
