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