mono — Mathlib

English

Let α be a complete lattice and s,t : ι → α. If s is an independent indexed family and t ≤ s componentwise, then t is independent.

Русский

Пусть α — полная решетка и s,t : ι → α. Если s образует независимую семью по индексу, и t по компонентам не превосходит s, то и t образует независимую семью.

LaTeX

$$$\\\\forall s,t: ι \\to α,\\\\ iSupIndep(s) \\\\land (t \\le s) \\\\Rightarrow iSupIndep(t)$$$

Lean4

theorem mono {s t : ι → α} (hs : iSupIndep s) (hst : t ≤ s) : iSupIndep t := fun i =>
  (hs i).mono (hst i) <| iSup₂_mono fun j _ => hst j

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