Theorems · Theorem · order theory
iSup_inf_iSup
∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α},
(⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
- Assumes
- Order.Frame
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- iSupstatement and proof · cited by 2,415
- Order.Framestatement and proof · cited by 88
- iSup_prodproof · cited by 10
- iSup_inf_eqproof · cited by 7
- inf_iSup_eqproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- iSup_inf_of_monotoneproof · cited by 3
- biSup_inf_biSupproof · cited by 2
- InfClosed.countableSupClosureproof · cited by 0