distortion_of_const — Mathlib

English

If every J in π has distortion = c and π.boxes is nonempty, then π.distortion = c.

Русский

Если для каждого J ∈ π выполняется distortion J = c и π.boxes непусто, то π.distortion = c.

LaTeX

$$$ π.boxes.Nonempty \rightarrow (\forall J \in π, J.distortion = c) \rightarrow π.distortion = c. $$$

Lean4

theorem distortion_of_const {c} (h₁ : π.boxes.Nonempty) (h₂ : ∀ J ∈ π, Box.distortion J = c) : π.distortion = c :=
  (sup_congr rfl h₂).trans (sup_const h₁ _)

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