frequently_and_distrib_right

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.frequently_and_distrib_right

← MathLib Explorer

English

The frequency of p x ∧ q is equivalent to (∃ᶠ x, p x) ∧ q.

Русский

Частотность p(x) ∧ q эквивалентна (∃ᶠ x, p x) ∧ q.

LaTeX

$$$ (\exists^\! x, p(x) \land q) \iff (\exists^\! x, p(x)) \land q $$$

Lean4

@[simp]
theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by simp only [@and_comm _ q, frequently_and_distrib_left]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru