lift — Mathlib

English

Lift an intermediate field of an intermediate field: given E ≤ F, the image E.map (val F) yields an intermediate field of L.

Русский

Поднять промежуточное поле внутри другого: E.map (val F) дает новое промежуточное поле в L.

LaTeX

$$$ \\text{lift} : \\text{IntermediateField}(K,L) \\to \\text{IntermediateField}(K,L) $$$

Lean4

/-- Lift an intermediate field of an intermediate field. -/
def lift {F : IntermediateField K L} (E : IntermediateField K F) : IntermediateField K L :=
  E.map (val F)

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