approx_le_approx_of_U_sub_C — Mathlib

English

If x lies in U-subset-C, then the comparison of approximations across c₁ and c₂ holds, with case distinction on membership of x in c₁.U.

Русский

Если x принадлежит U-подмножество-C, тогда сравнение аппроксимаций между c₁ и c₂ выполняется, с учётом принадлежности x к c₁.U.

LaTeX

$$$c_1.U \\subseteq c_2.C \\to \\forall x:\\; approx(n_2,c_2,x) \\le approx(n_1,c_1,x)$ при разборе по членству x в c_1.U.$$

Lean4

theorem approx_le_approx_of_U_sub_C {c₁ c₂ : CU P} (h : c₁.U ⊆ c₂.C) (n₁ n₂ : ℕ) (x : X) :
    c₂.approx n₂ x ≤ c₁.approx n₁ x := by
  by_cases hx : x ∈ c₁.U
  ·
    calc
      approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
      _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _
  ·
    calc
      approx n₂ c₂ x ≤ 1 := approx_le_one _ _ _
      _ = approx n₁ c₁ x := (approx_of_notMem_U _ _ hx).symm

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