supIndep_iff_disjoint_erase — Mathlib

English

SupIndep s f is equivalent to Disjoint (f i) ((s.erase i).sup f) for all i ∈ s, assuming decidable equality.

Русский

Эквивалентно: SupIndep s f эквивалентно Disjoint (f i) ((s.erase i).sup f) для всех i, при препятствии решаемости равенства.

LaTeX

$$$\\text{SupIndep}(s,f) \\iff \\forall i \\in s, Disjoint(f(i), (s \\setminus {i}).sup f).$$$

Lean4

/-- The RHS looks like the definition of `iSupIndep`. -/
theorem supIndep_iff_disjoint_erase [DecidableEq ι] : s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f) :=
  ⟨fun hs _ hi => hs (erase_subset _ _) hi (notMem_erase _ _), fun hs _ ht i hi hit =>
    (hs i hi).mono_right (sup_mono fun _ hj => mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩

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