mk_inv — Mathlib

English

For a set s in a group with involutive inverse, the cardinality of s⁻¹ equals cardinality of s.

Русский

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

LaTeX

$$$$ |s^{-1}| = |s| $$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by
  rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]

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