Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 19:22 50d1c485

View on Github →

feat(order/galois_connection): galois_coinsertions (#3656)

Estimated changes

Modified src/order/basic.lean

added theorem strict_mono_of_le_iff_le

modified theorem strict_mono_of_monotone_of_injective

Modified src/order/galois_connection.lean

added def galois_coinsertion.dual

added theorem galois_coinsertion.l_injective

added theorem galois_coinsertion.l_le_l_iff

added def galois_coinsertion.lift_bounded_lattice

added def galois_coinsertion.lift_complete_lattice

added def galois_coinsertion.lift_lattice

added def galois_coinsertion.lift_order_bot

added def galois_coinsertion.lift_semilattice_inf

added def galois_coinsertion.lift_semilattice_sup

added def galois_coinsertion.monotone_intro

added def galois_coinsertion.of_dual

added theorem galois_coinsertion.strict_mono_l

added theorem galois_coinsertion.u_inf_l

added theorem galois_coinsertion.u_infi_l

added theorem galois_coinsertion.u_infi_of_lu_eq_self

added theorem galois_coinsertion.u_l_eq

added theorem galois_coinsertion.u_sup_l

added theorem galois_coinsertion.u_supr_l

added theorem galois_coinsertion.u_supr_of_lu_eq_self

added theorem galois_coinsertion.u_surjective

added structure galois_coinsertion

added def galois_connection.lift_order_top

added def galois_connection.to_galois_coinsertion

added def galois_connection.to_galois_insertion

added def galois_insertion.dual

deleted theorem galois_insertion.l_infi_of_ul

added theorem galois_insertion.l_infi_of_ul_eq_self

deleted theorem galois_insertion.l_supr_of_ul

added theorem galois_insertion.l_supr_of_ul_eq_self

added def galois_insertion.of_dual

added theorem galois_insertion.strict_mono_u

added theorem galois_insertion.u_le_u_iff