le_coe_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.le_coe_iff

English

For x ∈ WithTop(α) and a ∈ α, x ≤ a if and only if there exists a ∈ α with x = ↑a and a ≤ b.

Русский

Для x ∈ WithTop(α) и a ∈ α, x ≤ a эквивалентно существованию a' ∈ α such that x = ↑a' и a' ≤ a.

LaTeX

$$$x \le b \iff \exists a : \alpha, x = \uparrow a \land a \le b$$$

Lean4

theorem le_coe_iff : x ≤ b ↔ ∃ a : α, x = a ∧ a ≤ b := by simp [le_def]

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

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

Разделы

Аффилиация

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