principalOpen_le

Mathlib.Topology.Sheaves.Alexandrov

URI: https://scilib.ai/kg/mathlib#Alexandrov.principalOpen_le

English

If x ≤ y, then principalOpen(y) ≤ principalOpen(x).

Русский

Если x ≤ y, то principalOpen(y) ≤ principalOpen(x).

LaTeX

$$$x \le y \Rightarrow \operatorname{principalOpen}(y) \le \operatorname{principalOpen}(x)$$$

Lean4

theorem principalOpen_le {x y : X} (h : x ≤ y) : principalOpen y ≤ principalOpen x := fun _ hc => le_trans h hc

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

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

Разделы

Аффилиация

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