English
If f ≤ g for partial equivalences M ≃ₚ[L] N, then f.symm ≤ g.symm; i.e., taking inverses reverses the order in this sense.
Русский
Если f ≤ g для частичных эквив между M и N, тогда f.symm ≤ g.symm; то есть обращение сохраняет отношение порядка в обратном виде.
LaTeX
$$$\forall L\ M\ N\ [L\text{ Structure }M]\ [L\text{ Structure }N],\\
\forall f,g : M \equiv_p^L N,\ f \le g \rightarrow f^{\mathrm{symm}} \le g^{\mathrm{symm}}.$$$
Lean4
@[gcongr]
theorem symm_le_symm {f g : M ≃ₚ[L] N} (hfg : f ≤ g) : f.symm ≤ g.symm :=
by
rw [le_iff]
refine ⟨cod_le_cod hfg, dom_le_dom hfg, ?_⟩
intro x
apply g.toEquiv.injective
change g.toEquiv (inclusion _ (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm _)
rw [g.toEquiv.apply_symm_apply, (Equiv.apply_symm_apply f.toEquiv x).symm, f.toEquiv.symm_apply_apply]
exact toEquiv_inclusion_apply hfg _
