inv_sup — Mathlib

English

For submonoids S,T, the inverse of their supremum equals the supremum of their inverses: (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹.

Русский

Для подмономоидов S и T обратная сверху (sup) равна верхнему пределу обратных: (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹.

LaTeX

$$$(S \\sqcup T)^{-1} = S^{-1} \\sqcup T^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_sup (S T : Submonoid G) : (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹ :=
  (invOrderIso : Submonoid G ≃o Submonoid G).map_sup S T

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