iInf_singleton — 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_singleton (a : α) (s : α → β) : ⨅ x ∈ ({ a } : Finset α), s x = s a := by simp

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