Commit 2021-11-30 10:08 6102d771

View on Github →

feat(group_theory/submonoid/pointwise): pointwise inverse of a submonoid (#10451) This also adds order_iso.map_{supr,infi,Sup,Inf} which are used here to provide some short proofs.

Estimated changes

Modified src/algebra/pointwise.lean

added theorem set.Inter_inv

added theorem set.Union_inv

Modified src/group_theory/submonoid/pointwise.lean

added theorem submonoid.closure_inv

added theorem submonoid.coe_inv

added theorem submonoid.inv_bot

added theorem submonoid.inv_inf

added theorem submonoid.inv_infi

added theorem submonoid.inv_le

added theorem submonoid.inv_le_inv

added def submonoid.inv_order_iso

added theorem submonoid.inv_sup

added theorem submonoid.inv_supr

added theorem submonoid.inv_top

added theorem submonoid.mem_inv

Modified src/order/complete_lattice.lean

added theorem order_iso.map_Inf

added theorem order_iso.map_Sup

added theorem order_iso.map_infi

added theorem order_iso.map_supr