mk_preimage_sigma

Mathlib.Data.Set.Sigma

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

English

For hi ∈ s, the preimage of s.sigma t under Sigma.mk i is t i.

Русский

Пусть hi ∈ s. Тогда предобраз Sigma.mk i от s.sigma t равен t i.

LaTeX

$$$\text{mk_preimage_sigma} (hi) :\; \Sigma.mk i^{-1}' (s.sigma t) = t i$$$

Lean4

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

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

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

Разделы

Аффилиация

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