sigma_mk_preimage_image' — Mathlib

English

If i ≠ j, then the preimage of the i-indexed image under Sigma.mk j is empty.

Русский

Если индексы i и j различны, то прообраз изображения по Sigma.mk j пуст.

LaTeX

$$$\{ x : (\beta_i) \} \; \text{не содержит элементы из} \; (\Sigma\mathrm{mk}\, j)^{-1} (\Sigma\mathrm{mk}\, i \;''\; s) = \emptyset$, при $i \neq j$$$

Lean4

theorem sigma_mk_preimage_image' (h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅ := by simp [image, h]

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