wellFoundedLT_dual_iff

Mathlib.Order.RelClasses

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

English

For any α with LT, WellFoundedLT(OrderDual α) is equivalent to WellFoundedGT α.

Русский

Для любого α с LT WellFoundedLT(OrderDual α) эквивалентно WellFoundedGT α.

LaTeX

$$$(\\mathrm{WellFoundedLT}(\\mathrm{OrderDual}\\ α) \\iff \\mathrm{WellFoundedGT} α)$$$

Lean4

theorem wellFoundedLT_dual_iff (α : Type*) [LT α] : WellFoundedLT αᵒᵈ ↔ WellFoundedGT α :=
  ⟨fun h => ⟨h.wf⟩, fun h => ⟨h.wf⟩⟩

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

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

Разделы

Аффилиация

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