English
The infimum of two filters is the filter generated by intersections of their elements.
Русский
Наименьшее верхнее ограничение двух фильтров есть фильтр, порождаемый пересечениями элементов этих фильтров.
LaTeX
$$infimum(f,g) = { s | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b }$$
Lean4
/-- The infimum of filters is the filter generated by intersections
of elements of the two filters. -/
instance instInf : Min (Filter α) :=
⟨fun f g : Filter α =>
{ sets := {s | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b}
univ_sets := ⟨_, univ_mem, _, univ_mem, by simp⟩
sets_of_superset := by
rintro x y ⟨a, ha, b, hb, rfl⟩ xy
refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y, mem_of_superset hb subset_union_left, ?_⟩
rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]
inter_sets := by
rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩
refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
ac_rfl }⟩
