forgetToBoolAlgFaithful — Mathlib

English

The forgetful functor forget₂ FinBoolAlg BoolAlg is faithful; morphisms are determined by their underlying Boolean-algebra maps.

Русский

Функтор забывания forget₂ FinBoolAlg BoolAlg верен; морфизмы определяются своими базисными отображениями булевых алгебр.

LaTeX

$$$ \\operatorname{Faithful}(\\mathrm{forget}_2) $$$

Lean4

instance forgetToBoolAlgFaithful : (forget₂ FinBoolAlg BoolAlg).Faithful :=
  InducedCategory.faithful _

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