mem_interior — Mathlib

English

A filter l belongs to the interior of a set s of filters iff there exists t ∈ l with Iic(𝓟 t) ⊆ s.

Русский

Фильтр l принадлежит внутренности множества s фильтров тогда и только тогда, когда существует t ∈ l с Iic(𝓟 t) ⊆ s.

LaTeX

$$$\forall {l : \text{Filter}(\alpha), {s : \text{Set}(\text{Filter}(\alpha))},\; l \in \operatorname{interior}(s) \iff \exists t \in l, Iic(\mathcal{P} t) \subseteq s.$$$

Lean4

protected theorem mem_interior {s : Set (Filter α)} {l : Filter α} : l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s := by
  rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

Похожие утверждения