mk_preimage_sigma_eq_if — Mathlib

English

With a decidable membership in s, Sigma.mk i⁻¹' s.sigma t equals t i if i ∈ s and equals ∅ otherwise.

Русский

При наличии решаемого членства i в s, предобраз Sigma.mk i от s.sigma t равен t i, если i ∈ s, и пустому множество иначе.

LaTeX

$$$[DecidablePred (\cdot \in s)] \; (\Sigma.mk i)^{-1}' (s.\sigma t) = \text{if } i \in s \text{ then } t i \text{ else } \emptyset$$$

Lean4

theorem mk_preimage_sigma_eq_if [DecidablePred (· ∈ s)] : Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅ := by
  grind

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