mem_lift — Mathlib

English

For any x in F, x belongs to lift E if and only if x belongs to E.

Русский

Для любого элемента x из F верно: x принадлежит lift(E) тогда и только тогда, когда x принадлежит E.

LaTeX

$$$\\forall x \\in F:\\; x \\in \\operatorname{lift}(E) \\iff x \\in E$$$

Lean4

theorem mem_lift {F : IntermediateField K L} {E : IntermediateField K F} (x : F) : x.1 ∈ lift E ↔ x ∈ E :=
  Subtype.val_injective.mem_set_image

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