threeGPFree_insert_of_lt — Mathlib

English

If every element of s is strictly less than a, inserting a into s preserves a GP-free structure in a two-way equivalence: ThreeGPFree(insert a s) holds exactly when ThreeGPFree s and the two compatibility conditions hold.

Русский

Если каждый элемент s строго меньше a, вставка a в s сохраняет GP-free структуру в двустороннем равенстве: ThreeGPFree(insert a s) эквивалентно ThreeGPFree s и двум условиям совместимости.

LaTeX

$$$\Big(\forall i\in s\, i

Lean4

@[to_additive]
theorem threeGPFree_insert_of_lt (hs : ∀ i ∈ s, i < a) :
    ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a * c = b * b → a = b :=
  by
  refine threeGPFree_insert.trans ?_
  rw [← and_assoc]
  exact and_iff_left fun b hb c hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim

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