isGLB_biInf — Mathlib

English

For s ⊆ β and f: β → α in a complete lattice, IsGLB(f''s) with the infimum ⨅_{x∈s} f(x) holds; i.e., IsGLB (f '' s) (⨅ x ∈ s, f x).

Русский

Для множества s ⊆ β и функции f: β → α в полной решётке выполняется: IsGLB (f'' s) (⨅ x∈s, f(x)).

LaTeX

$$$$ \operatorname{IsGLB}(f''s, \bigwedge_{x\in s} f(x)) $$$$

Lean4

theorem isGLB_biInf {s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ x ∈ s, f x) := by
  simpa only [range_comp, Subtype.range_coe, iInf_subtype'] using @isGLB_iInf α s _ (f ∘ fun x => (x : β))

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