mk_preimage_sigma_eq_empty

Mathlib.Data.Set.Sigma

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

English

If i ∉ s, then Sigma.mk i⁻¹' s.sigma t = ∅.

Русский

Если i ∉ s, то Sigma.mk i предобраз от s.sigma t пуст.

LaTeX

$$$i \notin s \implies (\Sigma.mk i)^{-1}' (s.\sigma t) = \emptyset$$$

Lean4

@[simp]
theorem mk_preimage_sigma_eq_empty (hi : i ∉ s) : Sigma.mk i ⁻¹' s.sigma t = ∅ := by grind

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

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

Разделы

Аффилиация

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