instPartialOrderPEquiv

Mathlib.Data.PEquiv

URI: https://scilib.ai/kg/mathlib#PEquiv.instPartialOrderPEquiv

Lean4

instance instPartialOrderPEquiv : PartialOrder (α ≃. β)
    where
  le f g := ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
  le_refl _ _ _ := id
  le_trans _ _ _ fg gh a b := gh a b ∘ fg a b
  le_antisymm f g fg
    gf :=
    ext
      (by
        intro a
        rcases h : g a with _ | b
        · exact eq_none_iff_forall_not_mem.2 fun b hb => Option.not_mem_none b <| h ▸ fg a b hb
        · exact gf _ _ h)

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

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

Разделы

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

Аффилиация

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