frequently_comap — Mathlib

English

A predicate p holds frequently along comap f l iff it holds frequently along l with a witness a such that f a = b and p a.

Русский

Справедливость p часто встречается на comap f l тогда и только если она часто встречается на l с свидетельством a, удовлетворяющим f a = b и p a.

LaTeX

$$(∃ᶠ a in comap f l, p a) ↔ ∃ᶠ b in l, ∃ a, f a = b ∧ p a$$

Lean4

@[simp]
theorem frequently_comap : (∃ᶠ a in comap f l, p a) ↔ ∃ᶠ b in l, ∃ a, f a = b ∧ p a := by
  simp only [Filter.Frequently, eventually_comap, not_exists, _root_.not_and]

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