inf'_eq_inf — Mathlib

English

Let s be a nonempty finite subset of β and f: β → α. The infimum with top-dual lattice equals the infimum in the dual: s.inf' H f = s.inf f, when considering αᵒᵈ.

Русский

Пусть s — непустое конечное подмножество β и f: β → α. Тогда inf' над s в двойственном порядке эквивалентен inf в обычном порядке: s.inf' H f = s.inf f, для αᵒᵈ.

LaTeX

$$$s \neq \varnothing \Rightarrow s.inf'(H,f) = s.inf f$ (в рамках αᵒᵈ)$$

Lean4

theorem inf'_eq_inf {s : Finset β} (H : s.Nonempty) (f : β → α) : s.inf' H f = s.inf f :=
  sup'_eq_sup (α := αᵒᵈ) H f

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