restrict_mono — Mathlib

English

Restricting a prepartition to itself yields the same prepartition.

Русский

Ограничение предразбиения самим собой даёт то же предразбиение.

LaTeX

$$$ \\text{restrict\_self}: \\; π.restrict I = π $$$

Lean4

@[mono]
theorem restrict_mono {π₁ π₂ : Prepartition I} (Hle : π₁ ≤ π₂) : π₁.restrict J ≤ π₂.restrict J := by
  classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

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