isBlock_iff_smul_eq_smul_of_nonempty

English

A block is characterized by the property that whenever the intersection of g1•B and g2•B is nonempty, the two images are equal.

Русский

Блок эквивалентен свойству: пересечение образов непусто тогда и только тогда, когда образы равны.

LaTeX

$$IsBlock G B ↔ ∀ {g1 g2 : G}, (g1 • B ∩ g2 • B).Nonempty → g1 • B = g2 • B$$

Lean4

@[to_additive]
theorem isBlock_iff_smul_eq_smul_of_nonempty :
    IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B := by
  simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

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