mem_of_liesOver — Mathlib

English

If P = Q.comap f and Q lies over p, then P lies over p. Contraction along f preserves LiesOver under an equality of comaps.

Русский

Если P = Q.comap f и Q лежит над p, то P лежит над p. Сжатие вдоль f сохраняет свойство LiesOver под равенством comap.

LaTeX

$$$ P = Q\\, .comap\\, f \\quad \\text{and} \\quad Q.LiesOver p \\;\\Rightarrow\\; P.LiesOver p. $$$

Lean4

theorem mem_of_liesOver [P.LiesOver p] (x : A) : x ∈ p ↔ algebraMap A B x ∈ P :=
  by
  rw [P.over_def p]
  rfl

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