eventually_map — Mathlib

English

For any f on α, m: α → β, the filter map commutes with eventually quantified predicates: (∀ᶠ b in map m f, P b) ⇔ ∀ᶠ a in f, P(m a).

Русский

Пусть есть фильтр f на α и отображение m: α → β. Тогда свойство, справедливое позднее, сохраняется: (∀ᶠ b в map m f, P b) ⇔ ∀ᶠ a в f, P(m a).

LaTeX

$$$(\\forall\\!\\!\\! b \\in map m f, P b) \\;\\iff\\; (\\forall\\!\\!\\! a \\in f, P (m a))$$$

Lean4

@[simp]
theorem eventually_map {P : β → Prop} : (∀ᶠ b in map m f, P b) ↔ ∀ᶠ a in f, P (m a) :=
  Iff.rfl

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