ext — Mathlib

English

Two closure operators are equal if they agree on all inputs; i.e., extensionality principle.

Русский

Два оператора замыкания равны, если они дают одинаковый результат на каждом аргументе.

LaTeX

$$$\forall c_1,c_2: ClosureOperator(\\alpha), (\\forall x:\\alpha, c_1(x)=c_2(x)) \\Rightarrow c_1=c_2$$$

Lean4

@[ext]
theorem ext : ∀ c₁ c₂ : ClosureOperator α, (∀ x, c₁ x = c₂ x) → c₁ = c₂ :=
  DFunLike.ext

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