image_inter_image_iff — Mathlib

English

The intersection of the quotient images of U and V is empty if and only if no x∈U has any g with g·x∈V.

Русский

Пересечение образов U и V в фактор-представлении пусто тогда и только тогда, когда для всех x∈U и любого g∈G нет такого g·x∈V.

LaTeX

$$$\Quotient.mk' '' U \cap \Quotient.mk' '' V = \emptyset \iff \forall x \in U, \forall g \in G, g \cdot x \notin V$$$

Lean4

@[to_additive]
theorem image_inter_image_iff (U V : Set α) :
    letI := orbitRel G α
    Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V :=
  Set.disjoint_iff_inter_eq_empty.symm.trans disjoint_image_image_iff

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