mk_preimage_prod_right_eq_if — Mathlib

English

With decidable membership in s, Prod.mk a ⁻¹'(s × t) equals t if a ∈ s, otherwise ∅.

Русский

При наличии решения по принадлежности в s: Prod.mk a ⁻¹'(s × t) равно t если a ∈ s, иначе ∅.

LaTeX

$$$ (Prod.mk a)^{-1}'(s \times t) = \begin{cases} t & a \in s \\ emptyset & a \notin s \end{cases} $$$

Lean4

theorem mk_preimage_prod_right_eq_if [DecidablePred (· ∈ s)] : Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅ := by grind

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