le_collapse_of_insert_mem — Mathlib

English

If t = insert a s and t ∈ 𝒜 with a ∉ s, then f(t) ≤ collapse 𝒜 a f s; i.e., inserting a and compressing does not increase collapse.

Русский

Если t = insert a s и t ∈ 𝒜 с a ∉ s, то f(t) ≤ collapse 𝒜 a f s.

LaTeX

$$f( insert a s ) ≤ collapse(𝒜,a,f,s) when a ∉ s and t=insert a s ∈ 𝒜$$

Lean4

theorem le_collapse_of_insert_mem (ha : a ∉ s) (hf : 0 ≤ f) (hts : t = insert a s) (ht : t ∈ 𝒜) :
    f t ≤ collapse 𝒜 a f s := by
  rw [collapse_eq ha, ← hts, if_pos ht]
  split_ifs
  · exact le_add_of_nonneg_left <| hf _
  · rw [zero_add]

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