const_le_iff

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.const_le_iff

English

For every x,y in β, (↑x ≤ ↑y) iff x ≤ y, assuming NeBot l.

Русский

Для любых x,y в β, (↑x ≤ ↑y) эквивалентно x ≤ y, при условии NeBot l.

LaTeX

$$$(↑x :\\mathrm{Germ}(l,\\beta)) \\le ↑y \\iff x \\le y$$$

Lean4

@[simp, norm_cast]
theorem const_le_iff [LE β] [NeBot l] {x y : β} : (↑x : Germ l β) ≤ ↑y ↔ x ≤ y :=
  liftRel_const_iff

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

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

Разделы

Аффилиация

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