monotone_symm — Mathlib

English

The map sending a partial equivalence to its inverse is monotone with respect to the partial order on partial equivalences.

Русский

Перенос частичной эквив через инверсию монотонен относительно заданного порядка на частичных эквив.

LaTeX

$$$\text{Monotone}\big(\lambda f : M \equiv_p^L N,\ f^{\mathrm{symm}}\big).$$$

Lean4

theorem monotone_symm : Monotone (fun (f : M ≃ₚ[L] N) ↦ f.symm) := fun _ _ => symm_le_symm

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