iInf_union — Mathlib

English

For any f: β → α and subsets s, t ⊆ β, the infimum over s ∪ t equals the meet of the infima over s and t: ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ (⨅ x ∈ t, f x).

Русский

Для любых f: β → α и подмножеств s, t ⊆ β инфиминум по s ∪ t равен пересечению инфиминумов по s и по t.

LaTeX

$$$$ \\inf_{x \\in s \\cup t} f(x) = \\bigl( \\inf_{x \\in s} f(x) \\bigr) \\wedge \\bigl( \\inf_{x \\in t} f(x) \\bigr) $$$$

Lean4

theorem iInf_union {f : β → α} {s t : Set β} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x :=
  @iSup_union αᵒᵈ _ _ _ _ _

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