English
For H-subgroup, a and b lie in the same H-orbit around c iff their H-orbits coincide in α.
Русский
Для подгруппы H точки a и b лежат в одной орбите относительно c тогда и только тогда их орбиты H в α совпадают.
LaTeX
$$$ (a : α) ∈ MulAction.orbit H c \;\iff\; (b : α) ∈ MulAction.orbit H c$ given equality in Quotient$$
Lean4
@[to_additive]
theorem mem_subgroup_orbit_iff' {H : Subgroup G} {x : orbitRel.Quotient G α} {a b : x.orbit} {c : α}
(h : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧) : (a : α) ∈ MulAction.orbit H c ↔ (b : α) ∈ MulAction.orbit H c :=
by
simp_rw [mem_orbit_symm (a₂ := c)]
convert Iff.rfl using 2
rw [orbit_eq_iff]
suffices hb : ↑b ∈ orbitRel.Quotient.orbit (⟦a⟧ : orbitRel.Quotient H x.orbit)
by
rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq'] at hb
rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
convert hb using 1
rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
