iInf_range

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iInf_range

English

Let g: β → α and f: ι → β. Then the infimum over b in range f of g(b) equals the infimum over i of g(f(i)).

Русский

Пусть g: β → α и f: ι → β. Тогда inf_{b ∈ range f} g(b) = inf_i g(f(i)).

LaTeX

$$$\\\\bigwedge_{b \\in range f} g(b) = \\\\bigwedge_i g(f(i))$$$

Lean4

theorem iInf_range : ∀ {g : β → α} {f : ι → β}, ⨅ b ∈ range f, g b = ⨅ i, g (f i) :=
  @iSup_range αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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