inv_le — Mathlib

English

For submonoids S,T of a group, S⁻¹ ≤ T⁻¹ iff S ≤ T⁻¹; i.e., inversion reverses inclusion.

Русский

Для подмономоидов S, T группы выполняется S⁻¹ ≤ T⁻¹ тогда и только тогда, когда S ≤ T⁻¹; то есть инверсия обращает включение.

LaTeX

$$$S^{-1} \\le T^{-1} \\iff S \\le T^{-1}$$$

Lean4

@[to_additive]
theorem inv_le (S T : Submonoid G) : S⁻¹ ≤ T ↔ S ≤ T⁻¹ :=
  SetLike.coe_subset_coe.symm.trans Set.inv_subset

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