withTopEquiv_le — Mathlib

English

Let x, y be elements of PartENat. The top-extension map preserves and reflects order: for all x, y, withTopEquiv x ≤ withTopEquiv y if and only if x ≤ y.

Русский

Пусть x, y ∈ PartENat. Отображение верхнего завершения сохраняет и отражает порядок: для любых x, y верно, что withTopEquiv x ≤ withTopEquiv y тогда и только тогда, когда x ≤ y.

LaTeX

$$$ \operatorname{withTopEquiv}(x) \le \operatorname{withTopEquiv}(y) \iff x \le y $$$

Lean4

theorem withTopEquiv_le {x y : PartENat} : withTopEquiv x ≤ withTopEquiv y ↔ x ≤ y := by simp

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