bot — Mathlib

English

There is a bottom filter realizer obtained from the principal realizer on the empty set via ofEq principal_empty.

Русский

Существует реализатор нижнего фильтра, получаемый из principal_empty через ofEq.

LaTeX

$$$\\mathrm{Realizer.bot} = (\\mathrm{Realizer.principal}\\;\\emptyset).ofEq\\;\\mathrm{principal\\_empty}$.$$

Lean4

/-- `Unit` is a realizer for the bottom filter -/
protected def bot : (⊥ : Filter α).Realizer :=
  (Realizer.principal _).ofEq principal_empty

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