iSupIndep_def'' — Mathlib

English

A variant of the iSupIndep characterization using an explicit set of indices with a set-like supremum expression.

Русский

Вариант характеристик iSupIndep через явное множество индексов и sSup над множеством a.

LaTeX

$$iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup {a | ∃ j ≠ i, t j = a})$$

Lean4

theorem iSupIndep_def'' : iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup {a | ∃ j ≠ i, t j = a}) :=
  by
  rw [iSupIndep_def']
  aesop

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