orbit_fixingSubgroup_compl_subset

English

Membership in fixingSubgroup M s is equivalent to s being a subset of fixedBy m.

Русский

Членство в fixingSubgroup M s эквивалентно тому, что s ⊆ fixedBy α m.

LaTeX

$$$m \\in fixingSubgroup(M,s) \\iff s \\subseteq fixedBy(\\alpha,m)$$$

Lean4

/-- The orbit of the fixing subgroup of `sᶜ` (i.e. the moving subgroup of `s`) is a subset of `s` -/
@[to_additive]
theorem orbit_fixingSubgroup_compl_subset {s : Set α} {a : α} (a_in_s : a ∈ s) :
    MulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s :=
  by
  intro b b_in_orbit
  let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
  rw [Submonoid.mk_smul] at g_eq
  rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
  rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

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