mem_prepartition_iff — Mathlib

English

I ∈ prepartition n B iff there exists ν in admissibleIndex n B with box n ν = I.

Русский

I принадлежит предразбиению, если существует ν в admissibleIndex n B такое, что box n ν = I.

LaTeX

$$$I \in prepartition(n,B) \iff \exists ν ∈ admissibleIndex(n,B), box(n,ν) = I$$$

Lean4

@[simp]
theorem mem_prepartition_iff {B I : Box ι} : I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I := by
  classical rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]

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