eq_of_boxes_subset — Mathlib

English

If π1 is a partition and every box of π1 is also a box of π2, then π1 equals π2.

Русский

Если π1 — разбиение, и каждый блок π1 уже содержится в π2, тогда π1=π2.

LaTeX

$$$\\pi_1 \\text{IsPartition} \\; \\wedge\\; \\pi_1.{boxes} \\subseteq \\pi_2.{boxes} \\; \\Rightarrow\\; \\pi_1 = \\pi_2.$$$

Lean4

theorem eq_of_boxes_subset (h₁ : π₁.IsPartition) (h₂ : π₁.boxes ⊆ π₂.boxes) : π₁ = π₂ :=
  eq_of_boxes_subset_iUnion_superset h₂ <| h₁.iUnion_subset _

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