dExt — Mathlib

English

A dependent extension principle: if h relates domains and values, then f = g.

Русский

Зависимое правило расширения: если есть соответствия доменов и значений, то f = g.

LaTeX

$$$$f = g \Rightarrow \text{dExt}(...)$$$$

Lean4

/-- A dependent version of `ext`. -/
theorem dExt {f g : E →ₗ.[R] F} (h : f.domain = g.domain)
    (h' : ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y) : f = g :=
  ext h fun _ _ _ ↦ h' rfl

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