inv — Mathlib

English

For a Finset s, the inverse Finset s⁻¹ is the set of inverses of its elements: s⁻¹ = image (x ↦ x⁻¹) s.

Русский

Обратное Finset s состоит из обратных элементов каждого элемента s: s⁻¹ = образ x ↦ x⁻¹ от s.

LaTeX

$$$ s^{-1} = s.image (\lambda x. x^{-1}) $$$

Lean4

/-- The pointwise inversion of finset `s⁻¹` is defined as `{x⁻¹ | x ∈ s}` in scope `Pointwise`. -/
@[to_additive /-- The pointwise negation of finset `-s` is defined as `{-x | x ∈ s}` in scope `Pointwise`. -/
    ]
protected def inv : Inv (Finset α) :=
  ⟨image Inv.inv⟩

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