orderIsoIccZeroCoe_symm_apply_coe

English

For a ≥ 0 and b ∈ [0,a], the inverse image under the order isomorphism, when coerced to ℝ, equals b.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem orderIsoIccZeroCoe_symm_apply_coe (a : ℝ≥0) (b : Set.Iic a) : ((orderIsoIccZeroCoe a).symm b : ℝ) = b :=
  rfl

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