not_smul_set_ssubset_smul_set — Mathlib

English

Let G act on X and B be a G-block. Then for any g1, g2 in G, the translate g1·B is not a proper subset of the translate g2·B.

Русский

Пусть G действует на X и B является G-блоком. Тогда для любых g1, g2 ∈ G сдвиг g1·B не является строгим включением в sдвиг g2·B.

LaTeX

$$$\text{IsBlock}(G,B) \rightarrow \forall g_1,g_2\;\bigl(g_1\cdot B \subsetneq g_2\cdot B\bigr)^{-}.$$

Lean4

@[to_additive]
theorem not_smul_set_ssubset_smul_set (hB : IsBlock G B) : ¬g₁ • B ⊂ g₂ • B := fun hab ↦
  hab.ne <| hB.smul_eq_smul_of_subset hab.subset

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