isOpen_implies_isOpen_iff

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#isOpen_implies_isOpen_iff

English

For topologies t1,t2 on α, t2 ≤ t1 iff every t1-open set is t2-open.

Русский

Для топологий t1,t2 на α, t2 ≤ t1 тогда и только тогда, когда каждая открытая в t1 множество открыта в t2.

LaTeX

$$$(\\forall s, IsOpen[t_1] s \\rightarrow IsOpen[t_2] s) \\iff t_2 \\le t_1$$$

Lean4

theorem isOpen_implies_isOpen_iff : (∀ s, IsOpen[t₁] s → IsOpen[t₂] s) ↔ t₂ ≤ t₁ :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru