of_le — Mathlib

English

An abstraction of the left disjointness property to abstract fields with a tower of scalar extensions.

Русский

Абстракция разобщенности слева для абстрактных полей с каскадом расширений.

LaTeX

$$$A \perp L \Rightarrow A \perp L' \text{ for suitable }L'$$$

Lean4

/-- If `A` and `B` are linearly disjoint, `A'` and `B'` are contained in `A` and `B`,
respectively, then `A'` and `B'` are also linearly disjoint. -/
theorem of_le {A' B' : IntermediateField F E} (H : A.LinearDisjoint B) (hA : A' ≤ A) (hB : B' ≤ B) :
    A'.LinearDisjoint B' :=
  H.of_le_left hA |>.of_le_right hB

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