Theorems · Theorem · order theory
Set.Iic_subset_Iio
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊆ Set.Iio b ↔ a < b- Defined in
- Mathlib.Order.Interval.Set.Basic
- Cited by
- 12 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.
Cites6
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.Iiostatement and proof · cited by 1,166
- Set.Iicstatement and proof · cited by 1,111
- lt_of_le_of_ltproof · cited by 432
- Set.self_mem_Iicproof · cited by 26
Cited by12
Results whose statement or proof uses this declaration.
- WithTop.image_coe_Iicproof · cited by 4
- nhds_bot_basis_Iicproof · cited by 4
- WithTop.image_coe_Iocproof · cited by 3
- Filter.atBot_basis_Iioproof · cited by 3
- WithTop.image_coe_Iccproof · cited by 3
- InnerProductSpace.span_gramSchmidt_Iioproof · cited by 2
- nhdsLE_eq_iInf_inf_principalproof · cited by 1
- MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithinproof · cited by 1
- Nat.le_nthproof · cited by 1
- Filter.atBot_Iio_eqproof · cited by 1
- StieltjesFunction.measure_Iio_of_tendsto_atBot_atBotproof · cited by 1
- Filter.map_val_Iio_atBotproof · cited by 1