tower_bot — Mathlib

English

The LiesOver relation is compatible through towers: if 𝔓 lies over p, then P lies over p in the tower B over A and so on.

Русский

Соотношение LiesOver совместимо с тензорными башнями: если 𝔓 лежит над p, тогда P лежит над p в башне B над A и так далее.

LaTeX

$$$ \\text{LiesOver}(\\mathfrak{P}) \\text{ and } \\text{LiesOver}(P) \\Rightarrow \\text{LiesOver}(p). $$$

Lean4

theorem tower_bot [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p where
  over := by rw [𝔓.over_def p, 𝔓.over_def P, under_under]

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