ext_iff — Mathlib

English

f = g iff domains equal and they agree on all x.

Русский

f = g тогда и только тогда, когда области совпадают и они согласованы на всех x.

LaTeX

$$$$f = g \iff f.domain = g.domain \land \forall x, f x = g x.$$$$

Lean4

theorem ext_iff {f g : E →ₗ.[R] F} :
    f = g ↔ f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩ :=
  ⟨by rintro rfl; simp, fun ⟨deq, feq⟩ ↦ ext deq feq⟩

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