IsBlock — Mathlib

English

A set B is a G-block if for any g1,g2 ∈ G, g1•B ≠ g2•B implies they are disjoint.

Русский

Множество B является G-блоком, если для любых g1,g2 из G непустое пересечение их образов B означает равенство образов.

LaTeX

$$IsBlock G B := ∀ {g1 g2 : G}, g1 • B ≠ g2 • B → Disjoint (g1 • B) (g2 • B)$$

Lean4

/-- A set `B` is a `G`-block iff the sets of the form `g • B` are pairwise equal or disjoint. -/
@[to_additive /-- A set `B` is a `G`-block iff the sets of the form `g +ᵥ B` are pairwise equal or disjoint. -/
    ]
def IsBlock (B : Set X) :=
  ∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

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