ext — Mathlib

English

Equality of Equiv.Perm is determined by pointwise equality, i.e., extensionality for permutation equivalences.

Русский

Равенство Equiv.Perm определяется по значению на элементах: экстенсиональность для перестановок.

LaTeX

$$$\\forall {\\sigma \\tau : Equiv.Perm \\alpha}, (\\forall x, \\sigma x = \\tau x) \\Rightarrow \\sigma = \\tau.$$$

Lean4

@[ext]
theorem ext {σ τ : Equiv.Perm α} (H : ∀ x, σ x = τ x) : σ = τ :=
  Equiv.ext H

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