iInter_iInter_eq_right — Mathlib

English

Analogous to the left version, with the equality constraint on the other side: taking h with b = x yields s(b).

Русский

Аналогично левой версии, с ограничением по другой стороне: пересечение по h, где b = x, даёт s(b).

LaTeX

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

Lean4

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

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