and

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Eventually.and

English

If P and Q hold eventually (in f), then P ∧ Q holds eventually (in f).

Русский

Если P и Q выполняются eventually (в f), то P ∧ Q выполняется eventually (в f).

LaTeX

$$$f.Eventually p \\; f. Eventually q \\Rightarrow f. Eventually (p \\land q)$$$

Lean4

protected theorem and {p q : α → Prop} {f : Filter α} : f.Eventually p → f.Eventually q → ∀ᶠ x in f, p x ∧ q x :=
  inter_mem

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

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

Разделы

Аффилиация

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