Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 04:10 caed8413

View on Github →

feat(order/complete_lattice): add complete_lattice.independent.disjoint{_Sup,} (#6405)

Estimated changes

Modified src/order/compactly_generated.lean

Modified src/order/complete_lattice.lean

added theorem Inf_sup_le_infi_sup

added theorem complete_lattice.independent.disjoint

added theorem complete_lattice.independent.disjoint_Sup

modified theorem complete_lattice.independent.mono

modified def complete_lattice.independent

modified theorem complete_lattice.independent_empty

added theorem disjoint_Sup_left

added theorem disjoint_Sup_right

added theorem supr_inf_le_Sup_inf

Modified src/order/omega_complete_partial_order.lean