mk_preimage_prod_left_fn_eq_if — Mathlib

English

For [DecidablePred (· ∈ t)] (f : γ → α), (f a, b)^{-1}(s × t) equals (f^{-1}(s)) if b ∈ t, otherwise ∅.

Русский

Для [DecidablePred (∈ t)] (f : γ → α): (f a, b)^{-1}(s × t) = f^{-1}(s) если b ∈ t, иначе ∅.

LaTeX

$$$ (\text{preimage} (\lambda a, { fst := f a, snd := b }) (s \times t)) \\ = \\begin{cases} f^{-1}(s) & b \in t \\ ∅ & b \notin t \end{cases} $$$

Lean4

theorem mk_preimage_prod_left_fn_eq_if [DecidablePred (· ∈ t)] (f : γ → α) :
    (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅ := by grind

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