isBlock_iff_disjoint_smul_of_ne — Mathlib

English

A block is equivalent to the property that whenever g·B ∩ B is nonempty, then g·B = B.

Русский

Блок эквивалентен свойству: если g·B ∩ B ненулево, то g·B = B.

LaTeX

$$$IsBlock(G,B) \iff \forall g,\; (g\cdot B \cap B) \neq \emptyset \rightarrow g\cdot B = B.$$$

Lean4

@[to_additive]
theorem isBlock_iff_disjoint_smul_of_ne : IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B :=
  by
  refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩
  simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢
  exact hB h

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