map_le_iff_le_comap — Mathlib

English

For f: L →ₐ[K] L', s ∈ IntermediateField K L, and t ∈ IntermediateField K L', we have s.map f ≤ t if and only if s ≤ t.comap f.

Русский

Для отображения f: L →ₐ[K] L', промежуточного поля s в L и t в L', верно: s.map f ≤ t тогда и только тогда, когда s ≤ t.comap f.

LaTeX

$$$ s.map f \\le t \\iff s \\le t.comap f $$$

Lean4

theorem map_le_iff_le_comap {f : L →ₐ[K] L'} {s : IntermediateField K L} {t : IntermediateField K L'} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff

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