ext — Mathlib

English

Let f and g be principal-segment embeddings from r into s. If f(a) = g(a) for every a in α, then f = g.

Русский

Пусть f и g — главные секвенции (principal segment) отображений r в s. Если f(a) = g(a) для каждого a в α, то f = g.

LaTeX

$$$\\forall f,g:\\ PrincipaISeg(r,s),\\ (\\forall a:\\alpha,\\ f(a)=g(a)) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} (h : ∀ x, f x = g x) : f = g :=
  by
  rw [← toRelEmbedding_inj]
  ext
  exact h _

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