map_mono

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.map_mono

English

If S ≤ T as intermediate fields, then S.map f ≤ T.map f for any f.

Русский

Если S ⊆ T как промежуточные поля, то S.map f ⊆ T.map f для любого f.

LaTeX

$$$ S.map f \\le T.map f $$$

Lean4

theorem map_mono (f : L →ₐ[K] L') {S T : IntermediateField K L} (h : S ≤ T) : S.map f ≤ T.map f :=
  SetLike.coe_mono (Set.image_mono h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru