equiv_one — Mathlib

English

The left coset equivalence can be realized through the first coordinate of the complement equivalence.

Русский

Левая косет-эквивалентность реализуется через первую координату дополнения.

LaTeX

$$$ LeftCosetEquivalence K g ((hSK.equiv g).fst) $$$

Lean4

theorem equiv_one (hs1 : 1 ∈ S) (ht1 : 1 ∈ T) : hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩) := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]; simp [equiv]

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