lift_le — Mathlib

English

Let F be an intermediate field of L over K and E an intermediate field of F. Then the lift of E to L is contained in F.

Русский

Пусть F — промежуточное поле L над K, а E — промежуточное поле внутри F. Тогда подъем E в L удовлетворяет ⊂ F.

LaTeX

$$$\\operatorname{lift}(E) \\le F$$$

Lean4

theorem lift_le {F : IntermediateField K L} (E : IntermediateField K F) : lift E ≤ F :=
  by
  rintro _ ⟨x, _, rfl⟩
  exact x.2

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