mem_orbit_symm — Mathlib

English

For H ≤ G and x,y in orbit G x, a ∈ orbit H b iff (a as α) ∈ orbit H (b as α).

Русский

Для H ≤ G и элементов x,y из orbit G x, верно: a ∈ orbit H b и равносильно (a в α) ∈ orbit H (b в α).

LaTeX

$$$$ a \\in \\operatorname{orbit}(H, b) \\iff (a : \\alpha) \\in \\operatorname{orbit}(H, (b : \\alpha)). $$$$

Lean4

@[to_additive]
theorem mem_orbit_symm {a₁ a₂ : α} : a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁ := by simp_rw [← orbit_eq_iff, eq_comm]

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