Theorems · Theorem · order theory
ciSup_mem_iInter_Icc_of_antitone_Icc
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] [inst_1 : Preorder β]
[IsDirectedOrder β] {f g : β → α},
(Antitone fun n => Set.Icc (f n) (g n)) → (∀ (n : β), f n ≤ g n) → ⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty
closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- iSupstatement · cited by 2,415
- Set.Iccstatement and proof · cited by 1,702
- Set.iInterstatement · cited by 1,084
- Antitonestatement and proof · cited by 563
- IsDirectedOrderstatement and proof · cited by 316
- ConditionallyCompletePartialOrderSupstatement and proof · cited by 52
- Set.Icc_subset_Icc_iffproof · cited by 5
- Monotone.ciSup_mem_iInter_Icc_of_antitoneproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- BoxIntegral.Box.subbox_induction_on'proof · cited by 1