eventuallyConst_preimage — Mathlib

English

Preimages respect eventual constancy: the preimage of a set is eventually constant along l iff the set is constant along the image filter map f l.

Русский

Предобраз множества сохраняет EventuallyConst через отображение: EventuallyConst (f^{-1} s) л iff EventuallyConst s (map f l).

LaTeX

$$$\\\\forall {s : Set β} {f : α \\\\to β},\\\\; EventuallyConst (Set.preimage f s) l \\\\Leftrightarrow EventuallyConst s (\\\\text{map } f l)$$$

Lean4

theorem eventuallyConst_preimage {s : Set β} {f : α → β} : EventuallyConst (f ⁻¹' s) l ↔ EventuallyConst s (map f l) :=
  .rfl

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