iInf_sUnion — Mathlib

English

Let S be a set of sets and f a function into a complete lattice; the infimum over x in ⋃₀ S of f x equals the infimum over s in S and x in s of f x.

Русский

Пусть S — множество множеств и f — функция в полную решетку; инфиминум по x в ⋃₀ S f(x) равен инфиминуму по s∈S и x∈s f(x).

LaTeX

$$$\\big\\lceil \\;\\; \\text{iInf } x \\in \\bigcup_0 S f(x) = \\text{iInf}_{s \\in S} \\text{iInf}_{x \\in s} f(x) \\;\\rceil$$$

Lean4

theorem iInf_sUnion (S : Set (Set α)) (f : α → β) : (⨅ x ∈ ⋃₀ S, f x) = ⨅ (s ∈ S) (x ∈ s), f x := by
  rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

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