iInf_eq

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#IsGLB.iInf_eq

English

If there is a bijection e: ι ≃ ι' and g is related to f by g(e(x)) = f(x) for all x, then iInf f = iInf g.

Русский

Если есть биекция e: ι ≃ ι' и g связана с f тем, что g(e(x)) = f(x) для всех x, то iInf f = iInf g.

LaTeX

$$$$\\iInf_x f(x) = \\iInf_y g(y) \\quad\\text{if } g(e(x)) = f(x) \\text{ for all } x.$$$$

Lean4

theorem iInf_eq (h : IsGLB (range f) a) : ⨅ j, f j = a :=
  h.sInf_eq

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

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

Разделы

Аффилиация

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