eq_or_disjoint — Mathlib

English

The ranges of orbits are pairwise disjoint; more precisely, any two distinct orbit representatives give disjoint orbits.

Русский

Образы орбит попарно непересекаются; орбиты, соответствующие разным представителям, не пересекаются.

LaTeX

$$$\\{\\operatorname{orbit}(G,x)\\}_{x\\in X}$ образуют пару непересекаемых множеств; то есть диапазоны орбит параллельны.$$

Lean4

@[to_additive]
theorem eq_or_disjoint (a b : X) : orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b) :=
  by
  apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id
  simp +contextual only [Set.not_disjoint_iff, ← orbit_eq_iff, forall_exists_index, eq_comm, implies_true]

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