of_le_of_flat_left — Mathlib

English

If A ⟂ B and ha, hb are inclusions with flatness, then A' ⟂ B'.

Русский

Если A ⟂ B и A', B' включены и имеют плоскость, то A' ⟂ B'.

LaTeX

$$$A \\perp_L B \\Rightarrow (A' \\le A) \\Rightarrow (B' \\le B) \\Rightarrow A' \\perp_L B'$$$

Lean4

theorem of_le_of_flat_left {A' B' : Subalgebra R S} (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R A] [Module.Flat R B'] :
    A'.LinearDisjoint B' :=
  (H.of_le_right_of_flat hb).of_le_left_of_flat ha

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