eqOn_sup — Mathlib

English

If two maps f and g agree on two submodules S and T, they also agree on the supremum S ⊔ T of these submodules.

Русский

Если f и g совпадают на подмодулях S и T, то они совпадают на сумме (наибольшем верхнем пределе) S ⊔ T.

LaTeX

$$$(\\forall x \\in S, f(x) = g(x)) \\;\\land\\; (\\forall x \\in T, f(x) = g(x)) \\Rightarrow (\\forall x \\in S \\lor T, f(x) = g(x))$$$

Lean4

theorem eqOn_sup {f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : Set.EqOn f g ↑(S ⊔ T) :=
  by
  rw [← le_eqLocus] at hS hT ⊢
  exact sup_le hS hT

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