inv_inf — Mathlib

English

For a family S i of submonoids in a group G, the inverse of the infimum equals the infimum of the inverses: (⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹.

Русский

Для семейства S i подмономоидов в группе G обращение инвертирует наименьшее: (⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹.

LaTeX

$$(\\inf_i S_i)^{-1} = \\inf_i (S_i)^{-1}$$

Lean4

@[to_additive (attr := simp)]
theorem inv_inf (S T : Submonoid G) : (S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹ :=
  SetLike.coe_injective Set.inter_inv

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