Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 849ed4f9

View on Github →

feat(order/galois_connection): add Galois insertion and lattice lifts along a Galois insertion

Estimated changes

Modified analysis/measure_theory/measurable_space.lean

modified theorem measurable_space.comap_map_le

modified theorem measurable_space.le_map_comap

Modified order/filter.lean

modified theorem filter.le_vmap_map

modified theorem filter.map_vmap_le

Modified order/galois_connection.lean

deleted theorem galois_connection.decreasing_l_u

deleted theorem galois_connection.increasing_u_l

added theorem galois_connection.l_Sup

added theorem galois_connection.l_u_le

added theorem galois_connection.le_u_l

added def galois_connection.lift_order_bot

added theorem galois_connection.u_Inf

added def galois_insertion.lift_bounded_lattice

added def galois_insertion.lift_complete_lattice

added def galois_insertion.lift_lattice

added def galois_insertion.lift_order_top

added def galois_insertion.lift_semilattice_inf

added def galois_insertion.lift_semilattice_sup

added structure galois_insertion