orderIsoIccZeroCoe_apply_coe_coe — Mathlib

English

For a ≥ 0 and b ∈ [0,a], the underlying real of its image under the order isomorphism is exactly b.

Русский

Для a ≥ 0 и b ∈ [0,a], действительное число, лежащее в образе через изоморфизм порядка, равно b.

LaTeX

$$$ (\\operatorname{orderIsoIccZeroCoe} a \\; b : \\mathbb{R}) = b, \\quad b \\in [0,a]. $$$

Lean4

@[simp]
theorem orderIsoIccZeroCoe_apply_coe_coe (a : ℝ≥0) (b : Set.Icc (0 : ℝ) a) : (orderIsoIccZeroCoe a b : ℝ) = b :=
  rfl

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