ext — Mathlib

English

Two partial functions f and g are equal if they assign the same set of values to each input; i.e., for every a, b, b ∈ f(a) ↔ b ∈ g(a).

Русский

Две частичные функции f и g равны тогда и только тогда, когда для каждого входа a они дают одинаковые значения; то есть ∀ a, b, b ∈ f(a) ⇔ b ∈ g(a).

LaTeX

$$$\\forall a\\, b,\\ b \\in f(a) \\leftrightarrow b \\in g(a) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem ext {f g : α →. β} (H : ∀ a b, b ∈ f a ↔ b ∈ g a) : f = g :=
  funext fun a => Part.ext (H a)

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