ext — Mathlib

English

Two linear partial maps are equal if their domains coincide and they agree on all elements.

Русский

Два линейных частичных отображения равны, если их области совпадают и они совпадают на всех элементах.

LaTeX

$$$$\text{If } f\,\text{domain}=g\,\text{domain and } \forall x, f x = g x,\quad f=g.$$$$

Lean4

@[ext (iff := false)]
theorem ext {f g : E →ₗ.[R] F} (h : f.domain = g.domain)
    (h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩) : f = g :=
  by
  rcases f with ⟨f_dom, f⟩
  rcases g with ⟨g_dom, g⟩
  obtain rfl : f_dom = g_dom := h
  congr
  apply LinearMap.ext
  intro x
  apply h'

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