Theorems · Definition · order theory
Finset.Iio
{α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → α → Finset αThe finset $(-∞, b)$ of elements x such that x < b. Basically Set.Iio b as a finset.
- Defined in
- Mathlib.Order.Interval.Finset.Defs
- Cited by
- 147 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 5 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Preorderstatement and proof · cited by 7,952
- LocallyFiniteOrderBotstatement and proof · cited by 286
- LocallyFiniteOrderBot.finsetIioproof · cited by 1
Cited by152
Results whose statement or proof uses this declaration.
- disjointedproof · cited by 64
- Finset.coe_Iiostatement · cited by 34
- InnerProductSpace.gramSchmidtproof · cited by 30
- Finset.mem_Iiostatement · cited by 20
- MvPowerSeries.truncproof · cited by 9
- InnerProductSpace.gramSchmidt_orthogonalproof · cited by 6
- Finset.notMem_Iio_selfstatement and proof · cited by 6
- Nat.Iio_eq_rangestatement · cited by 6
- Finset.Iic_eq_cons_Iiostatement and proof · cited by 5
- partialSups_disjointedproof · cited by 5
- InnerProductSpace.gramSchmidt_defstatement and proof · cited by 5
- InnerProductSpace.mem_span_gramSchmidtproof · cited by 4