Theorems · Theorem · order theory
Set.Ici_subset_Ici
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊆ Set.Ici b ↔ b ≤ a- Defined in
- Mathlib.Order.Interval.Set.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext
- Assumes
- Preorder
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.
- Setstatement · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- Set.Icistatement and proof · cited by 1,070
- LE.le.trans'proof · cited by 140
- Set.self_mem_Iicproof · cited by 26
Cited by14
Results whose statement or proof uses this declaration.
- ScottContinuousOn.monotoneproof · cited by 5
- antitone_Iciproof · cited by 4
- IsTop.atTop_eqproof · cited by 4
- Filter.atTop_basis'proof · cited by 3
- ProbabilityTheory.Kernel.indep_limsup_atBot_selfproof · cited by 3
- Filter.hasAntitoneBasis_atTopproof · cited by 2
- Set.image_subtype_val_Ici_Iciproof · cited by 2
- intervalIntegral.integral_Ici_sub_Iciproof · cited by 2
- MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioiproof · cited by 2
- IsGLB.biUnion_Ici_eq_Iciproof · cited by 2
- isCountablyCompact_iff_countable_open_coverproof · cited by 1
- Filter.atTop_eq_generate_of_forall_exists_leproof · cited by 1