eqOn_closure — Mathlib

English

If the closure of a set s in L is the top substructure, and f,g agree on s, then they agree on the whole closure; hence f=g.

Русский

Если замыкание множества s в языке L равно верхнему подструктуру, и f и g согласованы на s, то они согласованы на замыкание, следовательно f=g.

LaTeX

$$$\\text{closure } L\\ s = \\top \\quad\\Rightarrow\\quad \\bigl(\\text{EqOn } f\\ g\\ s\\bigr) \\Rightarrow f=g$$$

Lean4

/-- If two `L.Hom`s are equal on a set, then they are equal on its substructure closure. -/
theorem eqOn_closure {f g : M →[L] N} {s : Set M} (h : Set.EqOn f g s) : Set.EqOn f g (closure L s) :=
  show closure L s ≤ f.eqLocus g from closure_le.2 h

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