instIsPretransitiveElemOrbit_1 — Mathlib

English

For any x in the quotient, x.orbit is pretransitive under G.

Русский

Для любого элемента x в фактор-множество, орбита x под действием G пре-транситивна.

LaTeX

$$∀ x : orbitRel.Quotient G α, IsPretransitive G x.orbit$$

Lean4

@[to_additive]
instance (x : orbitRel.Quotient G α) : IsPretransitive G x.orbit where
  exists_smul_eq := by
    induction x using Quotient.inductionOn'
    rintro ⟨y, yh⟩ ⟨z, zh⟩
    rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh
    rcases yh with ⟨g, rfl⟩
    rcases zh with ⟨h, rfl⟩
    refine ⟨h * g⁻¹, ?_⟩
    ext
    simp [mul_smul]

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