le_def — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem le_def {α} {t s : TopologicalSpace α} : t ≤ s ↔ IsOpen[s] ≤ IsOpen[t] :=
  Iff.rfl

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