toNNRealLinear_inj — Mathlib

English

The assignment Λ ↦ toNNRealLinear Λ is injective: if toNNRealLinear Λ1 = toNNRealLinear Λ2, then Λ1 = Λ2.

Русский

Отображение Λ ↦ toNNRealLinear Λ инъективно: если toNNRealLinear Λ1 = toNNRealLinear Λ2, то Λ1 = Λ2.

LaTeX

$$$ toNNRealLinear Λ_1 = toNNRealLinear Λ_2 \iff Λ_1 = Λ_2 $$$

Lean4

@[simp]
theorem toNNRealLinear_inj (Λ₁ Λ₂ : C_c(α, ℝ) →ₚ[ℝ] ℝ) : toNNRealLinear Λ₁ = toNNRealLinear Λ₂ ↔ Λ₁ = Λ₂ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  ext f
  rw [← nnrealPart_sub_nnrealPart_neg f]
  simp only [LinearMap.ext_iff, NNReal.eq_iff, toNNRealLinear_apply] at h
  simp_rw [map_sub, h]

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