isOpen_lt_prod — Mathlib

English

The set { (x,y) ∈ α×α | x < y } is open in α×α when α is linearly ordered with OrderClosedTopology.

Русский

Множество { (x,y) ∈ α×α | x < y } открыто в α×α для линейного порядка с OrderClosedTopology.

LaTeX

$$$ \\{(x,y) \\in \\alpha \\times \\alpha \\mid x < y\\} \\text{ is open on } \\alpha \\times \\alpha$$$

Lean4

theorem isOpen_lt_prod : IsOpen {p : α × α | p.1 < p.2} :=
  isOpen_lt continuous_fst continuous_snd

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