sSupIndep — Mathlib

English

An independent set in a complete lattice is a set such that each element is disjoint from the supremum of the rest.

Русский

Независимое множество в полной решётке — множество, у которого каждый элемент несовместим с supremum остального множества.

LaTeX

$$def sSupIndep (s : Set α) : Prop := ∀ a ∈ s, Disjoint a (sSup (s \\ {a}))$$

Lean4

/-- An independent set of elements in a complete lattice is one in which every element is disjoint
  from the `Sup` of the rest. -/
def sSupIndep (s : Set α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → Disjoint a (sSup (s \ { a }))

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