isBlock_iff_smul_eq_smul_or_disjoint

English

Block property is equivalent to, for any g1,g2, either g1•B = g2•B or they are disjoint.

Русский

Свойство блока эквивалентно: для любых g1,g2 либо их образы совпадают, либо непересекаются.

LaTeX

$$IsBlock G B ↔ ∀ g1 g2 : G, (g1 • B = g2 • B) ∨ Disjoint (g1 • B) (g2 • B)$$

Lean4

@[to_additive]
theorem isBlock_iff_smul_eq_smul_or_disjoint :
    IsBlock G B ↔ ∀ g₁ g₂ : G, g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B) :=
  forall₂_congr fun _ _ ↦ or_iff_not_imp_left.symm

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