English
If β has infimum, Germ l β inherits a semilatticeInf structure with inf defined pointwise by min on β.
Русский
Если β имеет инфимум, Germ l β наследует полосу полулогического Inf с inf определённым точечно как min на β.
LaTeX
$$$\\text{SemilatticeInf}(\\mathrm{Germ}_l \\beta)$ with $\\mathrm{inf}(f,g) = \\mathrm{Germ}(\\lambda x. f(x) \\;⊓\\; g(x))$$$
Lean4
instance instSemilatticeInf [SemilatticeInf β] : SemilatticeInf (Germ l β)
where
inf := min
inf_le_left f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ inf_le_left
inf_le_right f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ inf_le_right
le_inf f₁ f₂ g := inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ ↦ h₂.mp <| h₁.mono fun _x ↦ le_inf
