instHImp — Mathlib

English

There is a definable-implication operation on DefinableSet corresponding to Heyting implication in the Boolean algebra of definable sets.

Русский

Существует операция импликации на DefinableSet, соответствующая импликации Гейтинга в булевой алгебре определяемых множеств.

LaTeX

$$$$ (s \\Rightarrow t) \\text{ with underlying set equals } \\mathrm{himp}(s,t) \\text{ in the Boolean algebra of definable sets}. $$$$

Lean4

noncomputable instance instHImp : HImp (L.DefinableSet A α) where himp s t := ⟨s ⇨ t, s.2.himp t.2⟩

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