mk_preimage_sigma_fn_eq_if — Mathlib

English

For a function g, the preimage under (λ b, ⟨i, g b⟩) of s.sigma t equals if i ∈ s then preimage g (t i) else ∅.

Русский

Для функции g предобраз (λ b, ⟨i, g b⟩) от s.sigma t равен, если i ∈ s, предобраз g (t i), иначе пустое множество.

LaTeX

$$$\text{preimage} (\lambda b. \langle i, g b \rangle) (s.\sigma t) = \text{if } i \in s \text{ then } \text{preimage } g (t i) \text{ else } \emptyset$$$

Lean4

theorem mk_preimage_sigma_fn_eq_if {β : Type*} [DecidablePred (· ∈ s)] (g : β → α i) :
    (fun b ↦ Sigma.mk i (g b)) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅ := by grind

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