English
Let X be a topological space and l a filter on X with a basis consisting of open sets. Then the filter obtained by lifting interior along the basis equals l; i.e., the interior lift does not change the filter.
Русский
Пусть X — топологическое пространство, fильтр l на X имеет базис из открытых множеств. Тогда фильтр, получаемый поднимая внутрь по базису, совпадает с l; т.е. interior-подъем не изменяет фильтр.
LaTeX
$$$l.lift' interior = l$$$
Lean4
theorem lift'_interior_eq_self {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s)
(ho : ∀ i, p i → IsOpen (s i)) : l.lift' interior = l :=
le_antisymm l.lift'_interior_le <|
h.lift'_interior.ge_iff.2 fun i hi ↦ by simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi
