Source indexedlemma · leanprover/lean4:v4.32.0

BohrSet.add_subset_of_ewidth

APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:338 to 347

Mathematical statement

Exact Lean statement

lemma add_subset_of_ewidth [Finite G] {B₁ B₂ B₃ : BohrSet G}
    (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) :
    B₁.chordSet + B₂.chordSet ⊆ B₃.chordSet

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma add_subset_of_ewidth [Finite G] {B₁ B₂ B₃ : BohrSet G}    (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) :    B₁.chordSet + B₂.chordSet ⊆ B₃.chordSet := by  intro x  simp only [mem_chordSet_iff_nnnorm_ewidth, Set.mem_add, forall_exists_index, and_imp]  rintro x hx y hy rfl ψ  rw [map_add_eq_mul]  have : ‖1 - ψ x * ψ y‖₊ ≤ ‖1 - ψ x‖₊ + _ := nnnorm_one_sub_mul (by simp)  rw [←ENNReal.coe_le_coe, ENNReal.coe_add] at this  exact this.trans <| (h _).trans' <| add_le_add (hx _) (hy _)