le_iff — Mathlib

English

For a basis B, a topology t1 is below t2 iff every B-element is open in t1.

Русский

Для базиса B топология t1 лежит внутри t2 тогда, когда каждый элемент B открывается в t1.

LaTeX

$$$\text{IsBasis}(B) \Rightarrow (t_1 \le t_2) \iff \forall U \in B, \text{IsOpen}_{t_1}(U)$$$

Lean4

theorem le_iff {α} {t₁ t₂ : TopologicalSpace α} {Us : Set (Opens α)} (hUs : @IsBasis α t₂ Us) :
    t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] U := by
  conv_lhs => rw [hUs.eq_generateFrom]
  simp [Set.subset_def, le_generateFrom_iff_subset_isOpen]

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