ext — Mathlib

English

If two Heyting homomorphisms f and g agree on every element of α, then they are equal: f = g.

Русский

Если два гомоморфизма Хейтинга f и g согласны на каждом элементе α, то они равны: f = g.

LaTeX

$$$\\forall f,g:\\mathrm{HeytingHom}(\\alpha,\\beta),\\; (\\forall a:\\alpha,\\ f(a)=g(a)) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {f g : HeytingHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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