quotient_eq_of_quotient_subgroup_eq

English

A variant of equality of quotients under a subgroup after transporting with mk''.

Русский

Вариант равенства классов после переноса через mk''.

LaTeX

$$same as 122283$$

Lean4

@[to_additive]
theorem quotient_eq_of_quotient_subgroup_eq {H : Subgroup G} {a b : α} (h : (⟦a⟧ : orbitRel.Quotient H α) = ⟦b⟧) :
    (⟦a⟧ : orbitRel.Quotient G α) = ⟦b⟧ := by
  rw [@Quotient.eq] at h ⊢
  exact mem_orbit_of_mem_orbit_subgroup h

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