symm_le_iff — Mathlib

English

For partial equivalences f : M ≃ₚ[L] N and g : N ≃ₚ[L] M, we have f.symm ≤ g iff f ≤ g.symm.

Русский

Для частичных эквив f и g верно: f.symm ≤ g тогда и только тогда, когда f ≤ g.symm.

LaTeX

$$$\forall f : M \equiv_p^L N,\forall g : N \equiv_p^L M,\ (f^{\mathrm{symm}} \le g) \iff (f \le g^{\mathrm{symm}}).$$$

Lean4

theorem symm_le_iff {f : M ≃ₚ[L] N} {g : N ≃ₚ[L] M} : f.symm ≤ g ↔ f ≤ g.symm :=
  ⟨by intro h; rw [← f.symm_symm]; exact monotone_symm h, by intro h; rw [← g.symm_symm]; exact monotone_symm h⟩

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