inf_congr

Mathlib.Data.Finset.Lattice.Fold

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

English

The image f''s with s and s.inf f form a greatest lower bound: IsGLB (f''s) (s.inf f).

Русский

Изображение f''s вместе с s.inf f образуют наибольшую нижнюю грань: IsGLB (f''s) (s.inf f).

LaTeX

$$$ IsGLB (f'' s) (s.inf f) $$$

Lean4

theorem inf_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.inf f = s₂.inf g :=
  by
  subst hs
  exact Finset.fold_congr hfg

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

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

Разделы

Аффилиация

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