instSubsingletonOfIsEmpty — Mathlib

English

If α is a Boolean algebra with no elements, there is exactly one Boolean subalgebra of α; equivalently, the collection of Boolean subalgebras of α is a singleton.

Русский

Если α — булева алгебра, не имеющая элементов, существует ровно одна булева подалгебра α; эквивалентно: множество булевых подалгебр α состоит из одного элемента.

LaTeX

$$$\forall \alpha\ [BooleanAlgebra\ α]\ [IsEmpty\ α],\ Subsingleton(BooleanSubalgebra\ α)$$$

Lean4

instance [IsEmpty α] : Subsingleton (BooleanSubalgebra α) :=
  SetLike.coe_injective.subsingleton

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