sSupIndep_iff — Mathlib

English

For a set s in a complete lattice, sSupIndep s is equivalent to iSupIndep of the inclusion map from s into α.

Русский

Для множества s в полной решётке sSupIndep эквивалентно iSupIndep включения из s в α.

LaTeX

$$sSupIndep s ↔ iSupIndep ((↑) : s → α)$$

Lean4

theorem sSupIndep_iff {α : Type*} [CompleteLattice α] (s : Set α) : sSupIndep s ↔ iSupIndep ((↑) : s → α) :=
  by
  simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]
  refine forall₂_congr fun a ha => ?_
  simp [iSup_subtype, iSup_and]

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