equiv_fst_eq_self_of_mem_of_one_mem

English

If 1 ∈ T and g ∈ S, then the first component of hST.equiv g equals g.

Русский

Если 1 ∈ T и g ∈ S, тогда первая компонента hST.equiv g равна g.

LaTeX

$$$\forall g:\; (hST.equiv g).fst = g \,\text{ whenever } g\in S \text{ and } 1\in T.$$$

Lean4

theorem equiv_fst_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : (hST.equiv g).fst = ⟨g, hg⟩ :=
  by
  have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by rw [equiv, Equiv.ofBijective]; simp
  conv_lhs => rw [← this, Equiv.apply_symm_apply]

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