equiv_snd_eq_self_of_mem_of_one_mem

English

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

Русский

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

LaTeX

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

Lean4

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

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