English
If β has a multiplicative structure and ExistsMulOfLE property, then Germ l β also has ExistsMulOfLE, i.e., between any two germs f ≤ g there exists a germ h with f ≤ h ≤ g constructed compatibly with multiplication.
Русский
Если β имеет умножение и свойство ExistsMulOfLE, то Germ l β также имеет ExistsMulOfLE, то есть между любыми двух Герма f ≤ g существует Герм h такой, что f ≤ h ≤ g, совместимый с умножением.
LaTeX
$$$\\text{ExistsMulOfLE}(\\mathrm{Germ}_l \\beta)$$$
Lean4
@[to_additive]
instance instExistsMulOfLE [Mul β] [LE β] [ExistsMulOfLE β] : ExistsMulOfLE (Germ l β) where
exists_mul_of_le
{x
y} :=
inductionOn₂ x y fun f g (h : f ≤ᶠ[l] g) ↦ by
classical
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
filter_upwards [h] with x hx
rw [dif_pos hx, hc]
