English
ν is admissible for B iff box n ν ⊆ B.
Русский
ν является допустимым для B тогда, когда box n ν ⊆ B.
LaTeX
$$$ν ∈ admissibleIndex(n,B) \iff box(n,ν) ≤ B$$$
Lean4
/-- For `B : BoxIntegral.Box`, the `TaggedPrepartition` formed by the set of all
`unitPartition.box` whose index is `B`-admissible. -/
def prepartition (B : Box ι) : TaggedPrepartition B
where
boxes := Finset.image (fun ν ↦ box n ν) (admissibleIndex n B)
le_of_mem' _
hI := by
obtain ⟨_, hν, rfl⟩ := Finset.mem_image.mp hI
exact mem_admissibleIndex_iff.mp hν
pairwiseDisjoint _ hI₁ _ hI₂
h := by
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₁
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₂
exact disjoint.mp fun x ↦ h (congrArg (box n) x)
tag I := if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else B.exists_mem.choose
tag_mem_Icc
I := by
by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
· simp_rw [dif_pos hI]
exact Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)
· simp_rw [dif_neg hI]
exact Box.coe_subset_Icc B.exists_mem.choose_spec
