inf_cons

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.inf_cons

English

If b ∉ s, then inf over cons b s f equals f(b) ⊓ inf over s f.

Русский

Если b не принадлежит s, то infimum по объединению (cons) b с s равен f(b) ∧ inf f над s.

LaTeX

$$$ \operatorname{inf}(\operatorname{cons}(b,s,h),f) = f(b) \wedge \operatorname{inf}(s,f) $$$

Lean4

@[simp]
theorem inf_cons {b : β} (h : b ∉ s) : (cons b s h).inf f = f b ⊓ s.inf f :=
  @sup_cons αᵒᵈ _ _ _ _ _ _ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru