preimage_image_sigmaMk_of_ne

Mathlib.Data.Set.Sigma

URI: https://scilib.ai/kg/mathlib#Set.preimage_image_sigmaMk_of_ne

English

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

Русский

Если i ≠ j, то предобраз Sigma.mk i от образа Sigma.mk j '' s пуст.

LaTeX

$$$i \\neq j \\Rightarrow \\Sigma.mk i^{-1}'(\\Sigma.mk j '' s) = \\emptyset$$$

Lean4

theorem preimage_image_sigmaMk_of_ne (h : i ≠ j) (s : Set (α j)) : Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅ := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru