orderClosedTopology — Mathlib

English

For x ∈ ℂ, if x ≥ 0 in ComplexOrder then ‖x‖ = x.

Русский

Для x ∈ ℂ, если x ≥ 0 по ComplexOrder, то ‖x‖ = x.

LaTeX

$$$0 \\le x \\Rightarrow \\|x\\| = x$$$

Lean4

/-- We show that the partial order and the topology on `ℂ` are compatible.
We turn this into an instance scoped to `ComplexOrder`. -/
theorem orderClosedTopology : OrderClosedTopology ℂ where
  isClosed_le' := by
    simp_rw [le_def, Set.setOf_and]
    refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> continuity

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