forall_mem_single — Mathlib

English

For any p, the property p holds for all tagged elements in the singleton if and only if p holds for the pair (x,J).

Русский

Для любой p свойство p выполняется для всех помеченных элементов в единичном разбиении тогда и только тогда, когда p выполняется для пары (x,J).

LaTeX

$$$ (\forall J' \in \text{single}(I,J,hJ,x,h), p((\text{single}(I,J,hJ,x,h)).tag J')\,J') \iff p(x,J) $$$

Lean4

theorem forall_mem_single (p : (ι → ℝ) → Box ι → Prop) (hJ : J ≤ I) (h : x ∈ Box.Icc I) :
    (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J := by simp

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