inter

Mathlib.Order.SupClosed

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

English

If s and t are inf-closed, then their intersection s ∩ t is inf-closed.

Русский

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

LaTeX

$$$ (\\text{InfClosed } s) \\land (\\text{InfClosed } t) \\Rightarrow \\text{InfClosed}(s \\cap t) $$$

Lean4

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

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

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

Разделы

Аффилиация

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