finite_inv — Mathlib

English

For a type with involutive inverse, s⁻¹ is finite if and only if s is finite.

Русский

Для типа с инволютивной обратной операцией множество s⁻¹ конечное тогда и только тогда, когда s конечно.

LaTeX

$$$$ s^{-1}.Finite \\leftrightarrow s.Finite $$$$

Lean4

@[to_additive (attr := simp)]
theorem finite_inv : s⁻¹.Finite ↔ s.Finite := by rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]

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