inv — Mathlib

English

There is a pointwise inversion operation on sets: s⁻¹ = { x | x⁻¹ ∈ s }.

Русский

Существует покомпонентное обращение множества: s⁻¹ = { x | x⁻¹ ∈ s }.

LaTeX

$$$s^{-1} = \\{ x \\mid x^{-1} \\in s \\}$$$

Lean4

/-- The pointwise inversion of set `s⁻¹` is defined as `{x | x⁻¹ ∈ s}` in scope `Pointwise`. It is
equal to `{x⁻¹ | x ∈ s}`, see `Set.image_inv_eq_inv`. -/
@[to_additive /-- The pointwise negation of set `-s` is defined as `{x | -x ∈ s}` in scope `Pointwise`.
          It is equal to `{-x | x ∈ s}`, see `Set.image_neg_eq_neg`. -/
    ]
protected def inv [Inv α] : Inv (Set α) :=
  ⟨preimage Inv.inv⟩

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