isTopologicalBasis — Mathlib

English

The upper topology on α has a topological basis given by the upperBasis; equivalently, this basis is the dual of the lower basis on the dual order.

Русский

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

LaTeX

$$$\text{IsTopologicalBasis}(\text{upperBasis } \alpha)$$$

Lean4

protected theorem isTopologicalBasis : IsTopologicalBasis (upperBasis α) :=
  IsLower.isTopologicalBasis (α := αᵒᵈ)

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