and

Mathlib.Topology.Basic

URI: https://scilib.ai/kg/mathlib#IsOpen.and

English

The intersection of two open sets is open.

Русский

Пересечение двух открытых множеств открыто.

LaTeX

$$IsOpen {x | p1 x} → IsOpen {x | p2 x} → IsOpen {x | p1 x ∧ p2 x}$$

Lean4

theorem and : IsOpen {x | p₁ x} → IsOpen {x | p₂ x} → IsOpen {x | p₁ x ∧ p₂ x} :=
  IsOpen.inter

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

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

Разделы

Аффилиация

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