infinite_inv — Mathlib

English

Let α be a type with an involutive inverse. For any subset S ⊆ α, the inverse image S^{-1} has infinite cardinality if and only if S has infinite cardinality.

Русский

Пусть α — множество с операцией взятия обратного, инволютивной. Для любого подмножества S ⊆ α множество обратных элементов S^{-1} бесконечно тогда и только тогда, когда S бесконечно.

LaTeX

$$$(|S| = \\infty) \\iff (|S^{-1}| = \\infty)$$$

Lean4

@[to_additive (attr := simp)]
theorem infinite_inv : s⁻¹.Infinite ↔ s.Infinite :=
  finite_inv.not

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