Commit 2022-03-23 21:13 3b8d217c

View on Github →

refactor(order/upper_lower): Use ⨆ rather than Sup (#12644) Turn Sup (coe '' S) into ⋃ s ∈ S, ↑s and other similar changes. This greatly simplifies the proofs.

Estimated changes

Modified src/order/complete_boolean_algebra.lean

Modified src/order/complete_lattice.lean

Modified src/order/upper_lower.lean

added theorem lower_set.carrier_eq_coe

modified theorem lower_set.coe_Inf

modified theorem lower_set.coe_Sup

modified theorem lower_set.coe_infi

modified theorem lower_set.coe_infi₂

modified theorem lower_set.coe_supr

modified theorem lower_set.coe_supr₂

added theorem lower_set.mem_compl_iff

added theorem upper_set.carrier_eq_coe

modified theorem upper_set.coe_Inf

modified theorem upper_set.coe_Sup

modified theorem upper_set.coe_infi

modified theorem upper_set.coe_infi₂

modified theorem upper_set.coe_supr

modified theorem upper_set.coe_supr₂

added theorem upper_set.mem_compl_iff

Modified src/ring_theory/graded_algebra/homogeneous_ideal.lean

added theorem homogeneous_ideal.coe_bot

added theorem homogeneous_ideal.coe_inf

added theorem homogeneous_ideal.coe_sup

deleted theorem homogeneous_ideal.coe_supr

added theorem homogeneous_ideal.coe_top

modified theorem homogeneous_ideal.to_ideal_infi

added theorem homogeneous_ideal.to_ideal_infi₂

added theorem homogeneous_ideal.to_ideal_supr

added theorem homogeneous_ideal.to_ideal_supr₂

modified theorem ideal.is_homogeneous.Sup

added theorem ideal.is_homogeneous.infi₂

added theorem ideal.is_homogeneous.supr₂

Modified src/ring_theory/graded_algebra/radical.lean