inv_le_inv — Mathlib

English

There is an order isomorphism on submonoids given by inversion: Submonoid G ≃o Submonoid G with toEquiv := Equiv.inv _, map_rel_iff' := inv_le_inv.

Русский

Существует упорядоченное изоморфизм на подмономоидах, задаваемый инверсией: Submonoid G ≃o Submonoid G с toEquiv := Equiv.inv _, map_rel_iff' := inv_le_inv.

LaTeX

$$$\\text{invOrderIso} : \\text{Submonoid } G \\simeq_{o} \\text{Submonoid } G$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_le_inv (S T : Submonoid G) : S⁻¹ ≤ T⁻¹ ↔ S ≤ T :=
  SetLike.coe_subset_coe.symm.trans Set.inv_subset_inv

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