iInf_insert — Mathlib

English

For a ∈ α, Finset s and t: α → β, the infimum over insert a s satisfies: ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x.

Русский

Для элемента a, множества s и функции t: α → β верно: ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x.

LaTeX

$$$$\\displaystyle \\inf_{x \\in \\operatorname{insert}(a,s)} t(x) = t(a) \\wedge \\inf_{x \\in s} t(x). $$$$

Lean4

theorem iInf_insert (a : α) (s : Finset α) (t : α → β) : ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x :=
  @iSup_insert α βᵒᵈ _ _ _ _ _

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