instOrderTopologySubtypeReal — Mathlib

English

The irrational numbers, as a subset of ℝ, carry the induced order topology.

Русский

Иррациональные числа, как подмножество ℝ, несут индуцированную порядковую топологию.

LaTeX

$$$\operatorname{OrderTopology}(\{x \in \mathbb{R} \mid \operatorname{Irrational}(x)\})$$$

Lean4

instance : OrderTopology { x // Irrational x } :=
  induced_orderTopology _ Iff.rfl <|
    @fun _ _ hlt =>
      let ⟨z, hz, hxz, hzy⟩ := exists_irrational_btwn hlt
      ⟨⟨z, hz⟩, hxz, hzy⟩

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