filter_of_true

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.filter_of_true

English

Simplified variant: Eq (π.filter p) π holds when p is true for all J ∈ π.

Русский

Упрощённый вариант: равенство (π.filter p) π верно, если p истинно для всех J ∈ π.

LaTeX

$$$ (π.filter p) = π \text{ whenever } ∀ J \in π, p J. $$$

Lean4

theorem filter_of_true {p : Box ι → Prop} (hp : ∀ J ∈ π, p J) : π.filter p = π :=
  by
  ext J
  simpa using hp J

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

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

Разделы

Аффилиация

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