ext_on_codisjoint — Mathlib

English

If S and T are codisjoint submodules and f and g agree on S and on T, then f and g are identical on the entire domain.

Русский

Если S и T кодизо-сопоставимы и f, g согласованы на S и на T, то они совпадают на всем домене.

LaTeX

$$$Codisjoint(S,T) \\Rightarrow (EqOn f g S) \\land (EqOn f g T) \\Rightarrow f = g$$$

Lean4

theorem ext_on_codisjoint {f g : F} {S T : Submodule R M} (hST : Codisjoint S T) (hS : Set.EqOn f g S)
    (hT : Set.EqOn f g T) : f = g :=
  DFunLike.ext _ _ fun _ ↦ eqOn_sup hS hT <| hST.eq_top.symm ▸ trivial

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