toTopologicalSpace_le — Mathlib

English

For group topologies x,y, x.toTopologicalSpace ≤ y.toTopologicalSpace iff x ≤ y.

Русский

Для топологий группы x,y: x.toTopologicalSpace ≤ y.toTopologicalSpace тогда и только тогда, когда x ≤ y.

LaTeX

$$$x.toTopologicalSpace \\le y.toTopologicalSpace \\; \\iff \\; x \\le y$$$

Lean4

@[to_additive (attr := simp)]
theorem toTopologicalSpace_le {x y : GroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y :=
  Iff.rfl

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