ofDual_lt_ofDual_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.ofDual_lt_ofDual_iff

English

For x,y ∈ WithBot αᵒᵈ, WithBot.ofDual x < WithBot.ofDual y ⇔ y < x in the dualized setting.

Русский

Для x,y ∈ WithBot αᵒᵈ, WithBot.ofDual x < WithBot.ofDual y ⇔ y < x.

LaTeX

$$$ \mathrm{WithBot.ofDual}(x) < \mathrm{WithBot.ofDual}(y) \iff y < x. $$$$

Lean4

@[simp]
theorem ofDual_lt_ofDual_iff {x y : WithBot αᵒᵈ} : WithBot.ofDual x < WithBot.ofDual y ↔ y < x := by
  cases x <;> cases y <;> simp

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

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

Разделы

Аффилиация

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