coe_equiv_snd_eq_one_iff_mem — Mathlib

English

The second coordinate equals 1 if and only if the element lies in S given 1 ∈ T.

Русский

Вторая координата равна единице тогда и только тогда, когда элемент g лежит в S при условии 1 ∈ T.

LaTeX

$$$ ((hST.equiv g).snd) = 1 \iff g \in S \text{ (with } 1 \in T \text{)} $$$

Lean4

theorem coe_equiv_snd_eq_one_iff_mem {g : G} (h1 : 1 ∈ T) : ((hST.equiv g).snd : G) = 1 ↔ g ∈ S := by
  rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]

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