English
See earlier results: a block in a subgroup remains a block under appropriate conjugation or opposite action.
Русский
См. ранее: блок в подгруппе сохраняется как блок при соответствующем сопряжении или противодействующем действии.
LaTeX
$$$IsBlock\\ G\\ (s : Set H) \\Rightarrow IsBlock\\ G\\ (s : Set H)$$$
Lean4
/-- A block containing `a` is the orbit of `a` under its stabilizer -/
@[to_additive /-- A block containing `a` is the orbit of `a` under its stabilizer -/
]
theorem orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
MulAction.orbit (stabilizer G B) a = B := by
ext x
constructor
· rintro ⟨⟨k, k_mem⟩, rfl⟩
simp only [Subgroup.mk_smul]
rw [← k_mem, Set.smul_mem_smul_set_iff]
exact ha
· intro hx
obtain ⟨k, rfl⟩ := exists_smul_eq G a x
exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩
