mem_orbit_subMul_iff — Mathlib

English

For p, x, m ∈ p, x ∈ MulAction.orbit R m in p if and only if (x : M) ∈ MulAction.orbit R (m : M) in M.

Русский

Для p, x, m ∈ p, x принадлежит орбите m в p тогда и только тогда, когда (x : M) принадлежит орбите m в M.

LaTeX

$$$ x \\in \\mathrm{MulAction.orbit}\\ R\\ m \\iff (x : M) \\in \\mathrm{MulAction.orbit}\\ R\\ (m : M) $$$

Lean4

@[to_additive]
theorem mem_orbit_subMul_iff {p : SubMulAction R M} {x m : p} :
    x ∈ MulAction.orbit R m ↔ (x : M) ∈ MulAction.orbit R (m : M) := by rw [← val_preimage_orbit, Set.mem_preimage]

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