IsTrivialBlock — Mathlib

English

A trivial block is a subsingleton or the whole universe.

Русский

Простейший блок — это пододиночество или всё множество.

LaTeX

$$IsTrivialBlock B := B.Subsingleton ∨ B = univ$$

Lean4

/-- A trivial block is a `Set X` which is either a subsingleton or `univ`.

Note: It is not necessarily a block when the action is not by a group. -/
@[to_additive /-- A trivial block is a `Set X` which is either a subsingleton or `univ`.

    Note: It is not necessarily a block when the action is not by a group. -/
    ]
def IsTrivialBlock (B : Set X) :=
  B.Subsingleton ∨ B = univ

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