instInf — Mathlib

English

If β has a minimum operation, Germ l β inherits a minimum operation defined coordinatewise by taking the minimum of representatives.

Русский

Если β имеет операцию минимума, Germ l β наследует минимум, заданный по координатам как минимумы соответствующих представителей.

LaTeX

$$$\\text{Min}(\\mathrm{Germ}_l \\beta)$ with\\; \\mathrm{inf}(f,g) = \\mathrm{Germ}(l, \\beta)(x \\mapsto f(x) \\;⊓\\; g(x))$$$

Lean4

instance instInf [Min β] : Min (Germ l β) :=
  ⟨map₂ (· ⊓ ·)⟩

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