lowerSet_le_lower — Mathlib

English

If t1 and t2 are topologies on α with upper-lower structures, then t1 ≤ t2 holds under IsLowerSet and IsLower assumptions.

Русский

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

LaTeX

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

Lean4

theorem lowerSet_le_lower {t₁ t₂ : TopologicalSpace α} [@Topology.IsLowerSet α t₁ _] [@IsLower α t₂ _] : t₁ ≤ t₂ :=
  fun s hs => by
  rw [@isOpen_iff_isLowerSet α _ t₁]
  exact IsLower.isLowerSet_of_isOpen hs

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