biInf_sigma' — Mathlib

English

Let s ⊆ ι, t: ∀ i, Set(α i), and f: ∀ i, α i → β. Then the iterated infimum over i ∈ s and j ∈ t i equals the infimum over ij ∈ s.sigma t of f ij.fst ij.snd.

Русский

Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: ∀ i, α i → β. Тогда двойной инфимум по i ∈ s и j ∈ t i равен инфимуму по ij ∈ s.sigma t от f ij.fst ij.snd.

LaTeX

$$$\bigsqcap_{i \in s} \bigsqcap_{j \in t(i)} f(i,j) = \bigsqcap_{(i,j) \in s \sigma t} f(i,j)$$

Lean4

theorem _root_.biInf_sigma' (s : Set ι) (t : ∀ i, Set (α i)) (f : ∀ i, α i → β) :
    ⨅ (i ∈ s) (j ∈ t i), f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd :=
  Eq.symm (biInf_sigma _ _ _)

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