preimage_ite — Mathlib

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

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