gi — Mathlib · SciLib

English

Real.toNNReal and NNReal.toReal form a Galois insertion between ℝ and ℝ≥0.

Русский

Real.toNNReal и NNReal.toReal образуют зацепление Гало между ℝ и ℝ≥0.

LaTeX

$$$ \\mathrm{GI} = \\mathrm{GaloisInsertion}(\\operatorname{Real.toNNReal}, \\operatorname{NNReal.toReal}). $$$

Lean4

/-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion. -/
def gi : GaloisInsertion Real.toNNReal (↑) :=
  GaloisInsertion.monotoneIntro NNReal.coe_mono Real.toNNReal_monotone Real.le_coe_toNNReal fun _ => Real.toNNReal_coe

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