ext_iff — Mathlib

English

Two partial equivalences are equal iff there exists a domain equality and a pointwise agreement on that domain.

Русский

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

LaTeX

$$$f=g \iff \exists h_{dom}: f.dom = g.dom,\; \forall x: M,\forall h: x \in f.dom,\;\text{(compatibility condition)}.$$$

Lean4

theorem ext_iff {f g : M ≃ₚ[L] N} :
    f = g ↔
      ∃ h_dom : f.dom = g.dom,
        ∀ x : M, ∀ h : x ∈ f.dom, subtype _ (f.toEquiv ⟨x, h⟩) = subtype _ (g.toEquiv ⟨x, (h_dom ▸ h)⟩) :=
  by
  constructor
  · intro h_eq
    rcases f with ⟨dom_f, cod_f, equiv_f⟩
    cases h_eq
    exact ⟨rfl, fun _ _ ↦ rfl⟩
  · rintro ⟨h, H⟩; exact ext h H

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