mono

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.adjoin.mono

English

If T ⊇ S then adjoin F S ≤ adjoin F T.

Русский

Если T содержит S, то adjoin F S ⊆ adjoin F T.

LaTeX

$$$S \subseteq T \Rightarrow \operatorname{adjoin}_F S \le \operatorname{adjoin}_F T$$$

Lean4

@[mono, gcongr]
theorem mono (T : Set E) (h : S ⊆ T) : adjoin F S ≤ adjoin F T :=
  GaloisConnection.monotone_l gc h

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

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

Разделы

Аффилиация

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