English
Two quotient images of U and V are disjoint if and only if no element of U has its G-orbit meeting V.
Русский
Два образа U и V в фактор-множество по орбитам несовместны тогда и только тогда, когда никакой элемент из U не имеет пересечения своей орбитой с V.
LaTeX
$$$\text{Disjoint}(\Quotient.mk' '' U, \Quotient.mk' '' V) \iff \forall x \in U, \forall g \in G, g \cdot x \notin V$$$
Lean4
@[to_additive]
theorem disjoint_image_image_iff {U V : Set α} :
letI := orbitRel G α
Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V :=
by
letI := orbitRel G α
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
refine ⟨fun h a a_in_U g g_in_V => h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩
· simp
· intro h
rw [Set.disjoint_left]
rintro _ ⟨b, hb₁, hb₂⟩ ⟨c, hc₁, hc₂⟩
obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
exact h b hb₁ g hc₁
