coe_iSup₂ — Mathlib

English

The underlying set of the supremum over a double-indexed family f(i,j) is the intersection over i and j of the underlying sets of f(i,j).

Русский

Носитель объединения двойного индекса f(i,j) равен пересечению носителей всех f(i,j).

LaTeX

$$↑(iSup (f)) = ⋂ i, ⋂ j, ↑(f i j)$$

Lean4

@[norm_cast]
theorem coe_iSup₂ (f : ∀ i, κ i → UpperSet α) : (↑(⨆ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j := by simp

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