English
The preimage of an if-then-else is the if-then-else of the preimages: f^{-1}(s ? t1 : t2) = (f^{-1}(s) ? f^{-1}(t1) : f^{-1}(t2)).
Русский
Обратное образ условного выбора равно условному выбору обратных образов.
LaTeX
$$$f^{-1}(s.ite\ t1\ t2) = (f^{-1}(s)).ite\ (f^{-1}(t1))\ (f^{-1}(t2)).$$$
Lean4
@[simp]
theorem preimage_ite (f : α → β) (s t₁ t₂ : Set β) : f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂) :=
rfl