Commit 2022-12-19 23:59 c1efed93

View on Github →

feat: port Order.GaloisConnection (#1099)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/GaloisConnection.lean

added def GaloisCoinsertion.dual

added theorem GaloisCoinsertion.isGLB_of_l_image

added theorem GaloisCoinsertion.isLUB_of_l_image

added theorem GaloisCoinsertion.l_injective

added theorem GaloisCoinsertion.l_le_l_iff

added def GaloisCoinsertion.liftBoundedOrder

added def GaloisCoinsertion.liftCompleteLattice

added def GaloisCoinsertion.liftLattice

added def GaloisCoinsertion.liftOrderBot

added def GaloisCoinsertion.liftSemilatticeInf

added def GaloisCoinsertion.liftSemilatticeSup

added def GaloisCoinsertion.monotoneIntro

added def GaloisCoinsertion.ofDual

added theorem GaloisCoinsertion.strict_mono_l

added theorem GaloisCoinsertion.u_bsupᵢ_l

added theorem GaloisCoinsertion.u_bsupᵢ_of_lu_eq_self

added theorem GaloisCoinsertion.u_inf_l

added theorem GaloisCoinsertion.u_infᵢ_l

added theorem GaloisCoinsertion.u_infₛ_l_image

added theorem GaloisCoinsertion.u_l_eq

added theorem GaloisCoinsertion.u_l_leftInverse

added theorem GaloisCoinsertion.u_sup_l

added theorem GaloisCoinsertion.u_supᵢ_l

added theorem GaloisCoinsertion.u_supᵢ_of_lu_eq_self

added theorem GaloisCoinsertion.u_supₛ_l_image

added theorem GaloisCoinsertion.u_surjective

added structure GaloisCoinsertion

added theorem GaloisConnection.bddAbove_l_image

added theorem GaloisConnection.bddBelow_u_image

added theorem GaloisConnection.exists_eq_l

added theorem GaloisConnection.exists_eq_u

added theorem GaloisConnection.isGLB_l

added theorem GaloisConnection.isGLB_u_image

added theorem GaloisConnection.isGreatest_u

added theorem GaloisConnection.isLUB_l_image

added theorem GaloisConnection.isLUB_u

added theorem GaloisConnection.isLeast_l

added theorem GaloisConnection.l_bot

added theorem GaloisConnection.l_comm_iff_u_comm

added theorem GaloisConnection.l_comm_of_u_comm

added theorem GaloisConnection.l_eq

added theorem GaloisConnection.l_eq_bot

added theorem GaloisConnection.l_le

added theorem GaloisConnection.l_sup

added theorem GaloisConnection.l_supᵢ

added theorem GaloisConnection.l_supᵢ₂

added theorem GaloisConnection.l_supₛ

added theorem GaloisConnection.l_u_l_eq_l'

added theorem GaloisConnection.l_u_l_eq_l

added theorem GaloisConnection.l_u_le

added theorem GaloisConnection.l_u_le_trans

added theorem GaloisConnection.l_unique

added theorem GaloisConnection.le_iff_le

added theorem GaloisConnection.le_u

added theorem GaloisConnection.le_u_l

added theorem GaloisConnection.le_u_l_trans

added def GaloisConnection.liftOrderBot

added def GaloisConnection.liftOrderTop

added theorem GaloisConnection.lowerBounds_u_image

added theorem GaloisConnection.lt_iff_lt

added theorem GaloisConnection.monotone_intro

added theorem GaloisConnection.monotone_l

added theorem GaloisConnection.monotone_u

added def GaloisConnection.toGaloisCoinsertion

added def GaloisConnection.toGaloisInsertion

added theorem GaloisConnection.u_comm_of_l_comm

added theorem GaloisConnection.u_eq

added theorem GaloisConnection.u_eq_top

added theorem GaloisConnection.u_inf

added theorem GaloisConnection.u_infᵢ

added theorem GaloisConnection.u_infᵢ₂

added theorem GaloisConnection.u_infₛ

added theorem GaloisConnection.u_l_u_eq_u'

added theorem GaloisConnection.u_l_u_eq_u

added theorem GaloisConnection.u_top

added theorem GaloisConnection.u_unique

added theorem GaloisConnection.upperBounds_l_image

added def GaloisConnection

added def GaloisInsertion.dual

added theorem GaloisInsertion.isGLB_of_u_image

added theorem GaloisInsertion.isLUB_of_u_image

added theorem GaloisInsertion.l_binfᵢ_of_ul_eq_self

added theorem GaloisInsertion.l_binfᵢ_u

added theorem GaloisInsertion.l_bsupᵢ_u

added theorem GaloisInsertion.l_inf_u

added theorem GaloisInsertion.l_infᵢ_of_ul_eq_self

added theorem GaloisInsertion.l_infᵢ_u

added theorem GaloisInsertion.l_infₛ_u_image

added theorem GaloisInsertion.l_sup_u

added theorem GaloisInsertion.l_supᵢ_u

added theorem GaloisInsertion.l_supₛ_u_image

added theorem GaloisInsertion.l_surjective

added theorem GaloisInsertion.l_u_eq

added theorem GaloisInsertion.leftInverse_l_u

added def GaloisInsertion.liftBoundedOrder

added def GaloisInsertion.liftCompleteLattice

added def GaloisInsertion.liftLattice

added def GaloisInsertion.liftOrderTop

added def GaloisInsertion.liftSemilatticeInf

added def GaloisInsertion.liftSemilatticeSup

added def GaloisInsertion.monotoneIntro

added def GaloisInsertion.ofDual

added theorem GaloisInsertion.strict_mono_u

added theorem GaloisInsertion.u_injective

added theorem GaloisInsertion.u_le_u_iff

added structure GaloisInsertion

added theorem Nat.galois_connection_mul_div

added theorem OrderIso.bddAbove_image

added theorem OrderIso.bddAbove_preimage

added theorem OrderIso.bddBelow_image

added theorem OrderIso.bddBelow_preimage

added theorem OrderIso.to_galoisConnection

added def WithBot.giUnbot'Bot

added theorem infₛ_image2_eq_infₛ_infₛ

added theorem infₛ_image2_eq_infₛ_supₛ

added theorem infₛ_image2_eq_supₛ_infₛ

added theorem infₛ_image2_eq_supₛ_supₛ

added theorem supₛ_image2_eq_infₛ_infₛ

added theorem supₛ_image2_eq_infₛ_supₛ

added theorem supₛ_image2_eq_supₛ_infₛ

added theorem supₛ_image2_eq_supₛ_supₛ