dExt_iff — Mathlib

English

f = g iff there exists a domain equality and a pointwise equality after transporting along the equality.

Русский

f = g эквивалентно существованию равенства доменов и поперечному равенству по переносу вдоль этого равенства.

LaTeX

$$$$f = g \iff \exists deq, feq: (domain\equiv g.domain) \land (\forall x, f x = g y)$$$$

Lean4

theorem dExt_iff {f g : E →ₗ.[R] F} :
    f = g ↔ ∃ _domain_eq : f.domain = g.domain, ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y :=
  ⟨fun EQ =>
    EQ ▸
      ⟨rfl, fun x y h => by
        congr
        exact mod_cast h⟩,
    fun ⟨deq, feq⟩ => dExt deq feq⟩

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