himp

Mathlib.Topology.Constructible

URI: https://scilib.ai/kg/mathlib#Topology.IsConstructible.himp

English

If s and t are constructible, then the Heyting implication s ⇨ t is constructible.

Русский

Если s и t конструктивны, то импликация Heyting s ⇨ t конструктивна.

LaTeX

$$IsConstructible s → IsConstructible t → IsConstructible (s ⇨ t)$$

Lean4

theorem himp : IsConstructible s → IsConstructible t → IsConstructible (s ⇨ t) :=
  BooleanSubalgebra.himp_mem

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

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

Разделы

Аффилиация

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