English
A variant formulation of the previous bound, with the same qualitative conclusion.
Русский
Вариант формулировки предыдущего ограничения, сохраняющий тот же смысл.
LaTeX
$$$\\#({u\\in (atomise(s,F)).parts \\mid u\\subseteq t, u.Nonempty}) \\le 2^{(|F|-1)}$$$
Lean4
/-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
and each `β i` is ordered by `s`.
The `<` relation on `Lex (∀ i, β i)` is `Pi.Lex (· < ·) (· < ·)`, while the `<` relation on
`Colex (∀ i, β i)` is `Pi.Lex (· > ·) (· < ·)`. -/
protected def Lex (x y : ∀ i, β i) : Prop :=
∃ i,
(∀ j, r j i → x j = y j) ∧
s (x i)
(y i)
/- This unfortunately results in a type that isn't delta-reduced, so we keep the notation out of the
basic API, just in case -/
