wellFoundedGT_dual_iff

Mathlib.Order.RelClasses

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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