inter

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#SupClosed.inter

English

If s and t are sup-closed, then s ∩ t is sup-closed.

Русский

Если s и t sup-замкнуты, то их пересечение sup-замкнуто.

LaTeX

$$$$ \operatorname{supClosed}(s) \land \operatorname{supClosed}(t) \rightarrow \operatorname{supClosed}(s \cap t) $$$$

Lean4

theorem inter (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t) := fun _a ha _b hb ↦
  ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

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

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

Разделы

Аффилиация

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