Theorems · Theorem · order theory

Set.pi_univ_Ioc_update_left

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : DecidableEq ι] {x y : (i : ι) → α i}
  {i₀ : ι} {m : α i₀},
  x i₀ ≤ m →
    (Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i)) =
      {z | m < z i₀} ∩ Set.univ.pi fun i => Set.Ioc (x i) (y i)

Defined in: Mathlib.Order.Interval.Set.Pi
Cited by: 1 results in Mathlib
Foundations: Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Preorder DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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

Setstatement and proof · cited by 53,352
Preorderstatement and proof · cited by 7,952
Set.ofPredstatement and proof · cited by 6,101
Set.univstatement and proof · cited by 3,945
Compl.complproof · cited by 2,925
Set.Ioiproof · cited by 1,463
Set.Iicproof · cited by 1,111
Set.Iocstatement and proof · cited by 971
Function.updatestatement · cited by 502
Set.pistatement and proof · cited by 405
Set.inter_assocproof · cited by 67
Set.inter_eq_self_of_subset_leftproof · cited by 52

Cited by1

Results whose statement or proof uses this declaration.

Set.pi_univ_Ioc_update_unionproof · cited by 0