instHImp

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.carrier.instHImp

English

Sublocale carries a Heyting implication operation, defined by a ⇨ b ∈ S for a,b ∈ S.

Русский

Подлокаль имеет операцию импликации Гейтинга: для a,b ∈ S выполняется a ⇨ b ∈ S.

LaTeX

$$$(\forall a,b \in S)\; a \Rightarrow_S b \in S$$$

Lean4

instance instHImp : HImp S where himp a b := ⟨a ⇨ b, S.himp_mem b.2⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru