range_coeFn_eq — Mathlib

English

Two continuous semilinear maps are equal if they agree on all inputs.

Русский

Два непрерывных семилинейных отображения равны, если они согласованы на всех аргументах.

LaTeX

$$$\forall x,\; f x = g x\Rightarrow f=g$$$

Lean4

theorem range_coeFn_eq :
    Set.range ((⇑) : (M₁ →SL[σ₁₂] M₂) → (M₁ → M₂)) =
      {f | Continuous f} ∩ Set.range ((⇑) : (M₁ →ₛₗ[σ₁₂] M₂) → (M₁ → M₂)) :=
  by
  ext f
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.continuous, f, rfl⟩
  · rintro ⟨hfc, f, rfl⟩
    exact
      ⟨⟨f, hfc⟩, rfl⟩
        -- make some straightforward lemmas available to `simp`.

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