preimage_setOf_eq — Mathlib

English

The preimage of a set defined by a predicate equals the corresponding predicate applied after f.

Русский

Обратное образ множества, задаваемого свойством, равно множеству элементов, удовлетворяющих соответствующему свойству после применения f.

LaTeX

$$$f^{-1} \{ a \mid p(a) \} = \{ x \mid p(f(x)) \}.$$$

Lean4

@[simp]
theorem preimage_setOf_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} :=
  rfl

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