isOpen_cylinder

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.isOpen_cylinder

← MathLib Explorer

English

For any x and n, cylinder(x,n) is an open set.

Русский

Для любых x и n цилиндр(x,n) является открытым множеством.

LaTeX

$$$$ \mathrm{IsOpen}(\mathrm{cylinder}(x,n)) $$$$

Lean4

theorem isOpen_cylinder (x : ∀ n, E n) (n : ℕ) : IsOpen (cylinder x n) :=
  by
  rw [PiNat.cylinder_eq_pi]
  exact isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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