English
Infimum (greatest lower bound) of two CountableInterFilters l1 and l2 is CountableInterFilter (l1 ⊓ l2).
Русский
Наименьшее верхнее основание двух CountableInterFilter слияние через ⊓ сохраняется.
LaTeX
$$$\\text{countableInterFilter_inf}(l_1, l_2) : CountableInterFilter (l_1 \\ ⊓ \\ l_2)$$$
Lean4
/-- Infimum of two `CountableInterFilter`s is a `CountableInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
instance countableInterFilter_inf (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :
CountableInterFilter (l₁ ⊓ l₂) := by
refine ⟨fun S hSc hS => ?_⟩
choose s hs t ht hst using hS
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_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 _ _)
