mem_single — Mathlib

English

Let I and J be boxes with J ≤ I, and let x be a function ι → R with x ∈ Box.Icc I. Then the tagged prepartition single I J hJ x h contains exactly the single box J; i.e., the only element of the family is J.

Русский

Пусть I и J — коробки с J ≤ I, и пусть x : ι → R удовлетворяет x ∈ Box.Icc I. Тогда помеченное предварительное разбиение single I J hJ x h содержит ровно единственную коробку J; то есть единственный элемент семейства — это J.

LaTeX

$$$ J' \in \text{single}(I,J,hJ,x,h) \iff J' = J $$$

Lean4

@[simp]
theorem mem_single {J'} (hJ : J ≤ I) (h : x ∈ Box.Icc I) : J' ∈ single I J hJ x h ↔ J' = J :=
  Finset.mem_singleton

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