ext — Mathlib

English

Two partial equivalences with the same domain are equal if they agree on every point of that domain.

Русский

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

LaTeX

$$$f,g : M \equiv_p^L N\;\Rightarrow\; f.\mathrm{dom} = g.\mathrm{dom} \Rightarrow (\forall x\in f.\mathrm{dom}, \ f(x)=g(x)) \Rightarrow f=g.$$$

Lean4

theorem ext {f g : M ≃ₚ[L] N} (h_dom : f.dom = g.dom) :
    (∀ x : M, ∀ h : x ∈ f.dom, subtype _ (f.toEquiv ⟨x, h⟩) = subtype _ (g.toEquiv ⟨x, (h_dom ▸ h)⟩)) → f = g :=
  by
  intro h
  rcases f with ⟨dom_f, cod_f, equiv_f⟩
  cases h_dom
  apply le_antisymm <;> (rw [le_def]; use le_rfl; ext ⟨x, hx⟩)
  · exact (h x hx).symm
  · exact h x hx

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