closure_min

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#ClosureOperator.closure_min

← MathLib Explorer

English

If x ≤ y and y is closed, then c x ≤ y.

Русский

Если x ≤ y и y замкнуто, то c x ≤ y.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] {c : ClosureOperator {\\\\alpha}} \\\\forall {x y : {\\\\alpha}}, x \\\\le y \\\\Rightarrow c.IsClosed y \\\\Rightarrow c x \\\\le y$$$

Lean4

theorem closure_min (hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y :=
  hy.closure_le_iff.2 hxy

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

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

Разделы

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

Аффилиация

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