Theorems · Theorem · order theory
Set.iSup_iInf_of_monotone
Deprecated since 2026-02-03Use iSup_iInf_of_monotone instead.
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
[inst_3 : Order.Frame α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i jAlias of iSup_iInf_of_monotone.
- Defined in
- Mathlib.Data.Set.Finite.Lattice
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
- Finitestatement · cited by 3,029
- iSupstatement · cited by 2,415
- iInfstatement · cited by 1,690
- Monotonestatement · cited by 1,397
- IsDirectedOrderstatement · cited by 316
- Order.Framestatement · cited by 88
- iSup_iInf_of_monotoneproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.