mem_ofFixingSubgroup_insert_iff — Mathlib

English

Element x lies in fixingSubgroup after insertion iff it fixes a and lies in the previous fixingSubgroup.

Русский

Элемент x принадлежит fix Subgroup после вставки тогда и только тогда, когда он фиксирует a и принадлежит предыдущей fixingSubgroup.

LaTeX

$$$m\in fixingSubgroup M (insert a ( (fun x)\to x.val) '' s) \iff (\exists hx: x\in ofStabilizer M a, (⟨x,hx\rangle)\in fixingSubgroup (stabilizer M a) s)$$$

Lean4

@[to_additive]
theorem mem_ofFixingSubgroup_insert_iff {a : α} {s : Set (ofStabilizer M a)} {x : α} :
    x ∈ ofFixingSubgroup M (insert a ((fun x ↦ x.val) '' s)) ↔
      ∃ (hx : x ∈ ofStabilizer M a), (⟨x, hx⟩ : ofStabilizer M a) ∈ ofFixingSubgroup (stabilizer M a) s :=
  by
  simp_rw [mem_ofFixingSubgroup_iff, mem_ofStabilizer_iff]
  aesop

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