nnrealPart_coeFn_eq — Mathlib

English

The coarse description of nnrealPart aligns with the natural map Real → ℝ≥0, i.e., the underlying real-valued function of nnrealPart f is Real.to NNReal composed with f.

Русский

Базовое отображение nnrealPart совместимо с естественным отображением Real → ℝ≥0: подлежащая функция равна Real.toNNReal ∘ f.

LaTeX

$$$\forall f:\, \alpha \to^b \mathbb{R},\; (nnrealPart f)^{\wedge} = \mathrm{Real.toNNReal} \circ f.$$$

Lean4

@[simp]
theorem nnrealPart_coeFn_eq (f : α →ᵇ ℝ) : ⇑f.nnrealPart = Real.toNNReal ∘ ⇑f :=
  rfl

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