iInf_union — Mathlib

English

For Finset α, Finset β, and f: α → β, the infimum over the union equals the infimum of the two infima: ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ (⨅ x ∈ t, f x).

Русский

Для Finset α, Finset β и функции f верно: ⨅ x ∈ s ∪ t, f x = ⨅ x ∈ s, f x ⊓ ⨅ x ∈ t, f x.

LaTeX

$$$$\\displaystyle \\inf_{x \\in s \\cup t} f(x) = \\min\\left( \\inf_{x \\in s} f(x), \\inf_{x \\in t} f(x) \\right). $$$$

Lean4

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

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