coe_iInf₂ — Mathlib

English

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

Русский

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

LaTeX

$$↑(iInf (f)) = ⋃ i, ⋃ j, ↑(f i j)$$

Lean4

@[norm_cast]
theorem coe_iInf₂ (f : ∀ i, κ i → UpperSet α) : (↑(⨅ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j := by simp

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