Mathlib Map

Theorems · Definition · order theory

Set.uIoc

{α : Type u_1} → [LinearOrder α] → α → α → Set α

The open-closed uIcc with unordered bounds.

Defined in
Mathlib.Order.Interval.Set.UnorderedInterval
Cited by
182 results in Mathlib
Foundations
Depth 17 from the axioms, rests on 70 definitions · uses propext
Assumes
LinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.uIoc_of_le · cited by 38Set.uIoc_of_leintervalIntegrable_iff · cited by 29intervalIntegrable_iffmeasurableSet_uIoc · cited by 20measurableSet_uIocintervalIntegral.intervalIntegral_eq_integral_uIoc · cited by 17intervalIntegral.interval…Set.uIoc_subset_uIcc · cited by 15Set.uIoc_subset_uIccAbsolutelyContinuousOnInterval.disjWithin · cited by 15AbsolutelyContinuousOnInt…IntervalIntegrable.def' · cited by 14IntervalIntegrable.def'intervalIntegral.integral_congr_ae · cited by 10intervalIntegral.integral…Set.uIoc_eq_union · cited by 8Set.uIoc_eq_unionintervalIntegral.integral_add · cited by 7intervalIntegral.integral…intervalIntegral.intervalIntegrable_cpow' · cited by 7intervalIntegral.interval…Set.uIoc_comm · cited by 6Set.uIoc_commSet.uIoc_of_ge · cited by 6Set.uIoc_of_geintervalIntegral.continuousWithinAt_primitive · cited by 6intervalIntegral.continuo…IntervalIntegrable.congr_ae · cited by 6IntervalIntegrable.congr_…Set · cited by 53352SetLinearOrder · cited by 8572LinearOrderSet.Ioc · cited by 971Set.IocSet.uIocCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • LinearOrderstatement and proof · cited by 8,572
  • Set.Iocproof · cited by 971

Cited by183

Results whose statement or proof uses this declaration.