upperSet_le_upper — Mathlib

English

If t1 and t2 are topologies on α such that both are upper-set topologies, then t1 ≤ t2 in the lattice of topologies.

Русский

Если две топологии t1 и t2 на α являются топологиями верхних множеств, то t1 не хуже (≤) чем t2 в решетке топологий.

LaTeX

$$$$ t_1 \\le t_2. $$$$

Lean4

theorem upperSet_le_upper {t₁ t₂ : TopologicalSpace α} [@Topology.IsUpperSet α t₁ _] [@Topology.IsUpper α t₂ _] :
    t₁ ≤ t₂ := fun s hs => by
  rw [@isOpen_iff_isUpperSet α _ t₁]
  exact IsUpper.isUpperSet_of_isOpen hs

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