iInter_iInter_eq_left — Mathlib

English

If s is indexed by β with a bound b, then the iterated intersection over x and h with x=b reduces to s(b).

Русский

Если множество индексируется по β с границей b, то повторяющееся пересечение по x и h с x=b сводится к s(b).

LaTeX

$$$$\\bigcap_{x} \\bigcap_{h: x = b} s_xh = s_b\\,\\text{(with } h = \\text{refl}\\,\\text{)}$$$$

Lean4

@[simp]
theorem iInter_iInter_eq_left {b : β} {s : ∀ x : β, x = b → Set α} : ⋂ (x) (h : x = b), s x h = s b rfl :=
  iInf_iInf_eq_left

Похожие утверждения