BlockMem — Mathlib

English

The type BlockMem(a) collects all blocks that contain the element a.

Русский

Тип BlockMem(a) собирает все блоки, содержащие элемент a.

LaTeX

$$IsBlockMem(a) := { B : Set X // a ∈ B ∧ IsBlock G B }$$

Lean4

/-- The type of blocks for a group action containing a given element -/
@[to_additive /-- The type of blocks for an additive group action containing a given element -/
    ]
abbrev BlockMem (a : X) : Type _ :=
  { B : Set X // a ∈ B ∧ IsBlock G B }

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