lt_toDual_iff

Mathlib.Order.WithBot

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

← MathLib Explorer

English

For x ∈ WithTop αᵒᵈ and y ∈ WithBot α, x < toDual y is equivalent to y < ofDual x.

Русский

Для x ∈ WithTop αᵒᵈ и y ∈ WithBot α, x < toDual(y) эквивалентно y < ofDual(x).

LaTeX

$$$ x^{\mathrm{toDual}} < y \iff y < x^{\mathrm{toDual}}. $$$$

Lean4

theorem lt_toDual_iff {x : WithBot αᵒᵈ} {y : WithTop α} : x < WithTop.toDual y ↔ y < WithBot.ofDual x := by
  cases x <;> cases y <;> simp [lt_toDual]

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

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

Разделы

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

Аффилиация

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