disjoint_smul_set_smul — Mathlib

English

If B is a block and g·B is not contained in s·B, then g·B and s·B are disjoint.

Русский

Если B — блок, и g·B не содержится в s·B, то множества g·B и s·B не пересекаются.

LaTeX

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

Lean4

@[to_additive]
theorem disjoint_smul_set_smul (hB : IsBlock G B) (hgs : ¬g • B ⊆ s • B) : Disjoint (g • B) (s • B) :=
  by
  rw [← iUnion_smul_set, disjoint_iUnion₂_right]
  exact fun b hb ↦ hB fun h ↦ hgs <| h.trans_subset <| smul_set_subset_smul hb

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