Mathlib Map

Theorems · Theorem · order theory

Set.pi_univ_Icc

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i),
  (Set.univ.pi fun i => Set.Icc (x i) (y i)) = Set.Icc x y
Defined in
Mathlib.Order.Interval.Set.Pi
Cited by
11 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.image_update_Icc · cited by 7Set.image_update_IccReal.volume_Icc_pi · cited by 5Real.volume_Icc_piMeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc · cited by 3Measure.univ_pi_Ioc_ae_eq…Module.Basis.parallelepiped_basisFun · cited by 3Basis.parallelepiped_basi…BoxIntegral.Box.le_TFAE · cited by 2Box.le_TFAEMeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc · cited by 2Measure.univ_pi_Ioo_ae_eq…pi_Icc_mem_nhds · cited by 1pi_Icc_mem_nhdsMeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc · cited by 1Measure.univ_pi_Ico_ae_eq…BoxIntegral.Box.Icc_eq_pi · cited by 1Box.Icc_eq_pistdSimplex_subset_Icc · cited by 1stdSimplex_subset_IccSet.pi_univ_uIcc · cited by 0Set.pi_univ_uIccSet · cited by 53352SetPreorder · cited by 7952PreorderSet.univ · cited by 3945Set.univSet.ext · cited by 2266Set.extSet.Icc · cited by 1702Set.IccSet.pi · cited by 405Set.piSet.pi_univ_IccCITED BYCITES

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.univstatement · cited by 3,945
  • Set.extproof · cited by 2,266
  • Set.Iccstatement · cited by 1,702
  • Set.pistatement · cited by 405

Cited by11

Results whose statement or proof uses this declaration.