Theorems · Theorem · order theory
Set.iInf_iSup_of_monotone
Deprecated since 2026-02-03Use iInf_iSup_of_monotone instead.
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
[inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i jAlias of iInf_iSup_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
- IsCodirectedOrderstatement · cited by 95
- Order.Coframestatement · cited by 38
- iInf_iSup_of_monotoneproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.