disjoint_smul_smul_set — Mathlib

English

If B is a block and ¬(g·B ⊆ s·B), then s·B and g·B are disjoint.

Русский

Если B — блок и не выполняется включение g·B ⊆ s·B, то s·B и g·B не пересекаются.

LaTeX

$$$\text{IsBlock}(G,B) \rightarrow (\neg (g\cdot B \subseteq s\cdot B)) \rightarrow (s\cdot B) \cap (g\cdot B) = \emptyset.$$$

Lean4

@[to_additive]
theorem disjoint_smul_smul_set (hB : IsBlock G B) (hgs : ¬g • B ⊆ s • B) : Disjoint (s • B) (g • B) :=
  (hB.disjoint_smul_set_smul hgs).symm

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