posFittingCompOf_le_posFittingComp

English

For every x ∈ L, posFittingCompOf(R,M,x) is contained in posFittingComp(R,L,M).

Русский

Для каждого x ∈ L компонентa posFittingCompOf(R,M,x) содержится в posFittingComp(R,L,M).

LaTeX

$$$\operatorname{posFittingCompOf}(R,M,x) \leq \operatorname{posFittingComp}(R,L,M)$$$

Lean4

theorem posFittingCompOf_le_posFittingComp (x : L) : posFittingCompOf R M x ≤ posFittingComp R L M := by
  rw [posFittingComp]; exact le_iSup (posFittingCompOf R M) x

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