himp_le_iff

Mathlib.Order.CompleteBooleanAlgebra

URI: https://scilib.ai/kg/mathlib#himp_le_iff

English

In a frame, a ⇒ b ≤ c is equivalent to: for all d, if d ∧ a ≤ b then d ≤ c.

Русский

В рамке a ⇒ b ≤ c эквивалентно: для всех d, если d ∧ a ≤ b, тогда d ≤ c.

LaTeX

$$$a \Rightarrow b \le c \iff \forall d, (d \wedge a) \le b \rightarrow d \le c$$$

Lean4

theorem himp_le_iff : a ⇨ b ≤ c ↔ ∀ d, d ⊓ a ≤ b → d ≤ c := by
  simp [himp_eq_sSup]
    -- see Note [lower instance priority]

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

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

Разделы

Аффилиация

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