restrict_biUnion — Mathlib

English

Restricting the BiUnion to a fixed J recovers πi J.

Русский

Ограничение BiUnion к фиксированному J восстанавливает πi J.

LaTeX

$$$ (π.biUnion π_i).restrict J = π_i J $$$

Lean4

@[simp]
theorem restrict_biUnion (πi : ∀ J, Prepartition J) (hJ : J ∈ π) : (π.biUnion πi).restrict J = πi J :=
  by
  refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm
  · refine (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right ?_).symm⟩
    exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)
  · simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]
    rintro x ⟨hxJ, J₁, h₁, hx⟩
    obtain rfl : J = J₁ := π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)
    exact hx

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