embedBox — Mathlib

English

Same as IsHenstock.disjUnion with simplification.

Русский

То же самое, что IsHenstock.disjUnion с упрощениями.

LaTeX

$$$ IsHenstock(π_1.disjUnion π_2 h) \text{ (simp) } $$$

Lean4

/-- If `I ≤ J`, then every tagged prepartition of `I` is a tagged prepartition of `J`. -/
def embedBox (I J : Box ι) (h : I ≤ J) : TaggedPrepartition I ↪ TaggedPrepartition J
    where
  toFun
    π :=
    { π with
      le_of_mem' := fun J' hJ' => (π.le_of_mem' J' hJ').trans h
      tag_mem_Icc := fun J => Box.le_iff_Icc.1 h (π.tag_mem_Icc J) }
  inj' := by
    rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H
    simpa using H

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