mem_posFittingComp — Mathlib

English

An element m ∈ M lies in posFittingComp(R,L,M) exactly when it lies in the supremum of posFittingCompOf(R,M,x) over all x ∈ L.

Русский

Элемент m ∈ M принадлежит posFittingComp(R,L,M) тогда и только тогда, когда он принадлежит супремуму posFittingCompOf(R,M,x) по всем x ∈ L.

LaTeX

$$$m \in \operatorname{posFittingComp}(R,L,M) \iff m \in \bigvee_{x\in L} \operatorname{posFittingCompOf}(R,M,x)$$

Lean4

theorem mem_posFittingComp (m : M) : m ∈ posFittingComp R L M ↔ m ∈ ⨆ (x : L), posFittingCompOf R M x := by rfl

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