Research proof index

The transposed formulation of debate is the same

This is the dual of Dense.comap_val_nhdsWithin_Ioi_neBot.

This is an auxillary lemma used to prove Dense.monotone_of_isRightContinuous. It is saying that if D is a dense set and a, b are two points such that a < b, then the comap of 𝓝[Set.Ioi a] a under the inclusion D → α is nontrivial. Note that a < b is necessary as this is clearly not true if a is a top element.

If f is monotone on a dense set D and is right continuous, then f is monotone. We prove under the assumption that α has a top element ⊤ and ⊤ ∈ D, which is a necessary assumption because otherwise it is possible that ⊤ is an isolated point. This theorem should be also true when α satisfies NoTopOrder α.

If $X_1, X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$.

Let $T_1,T_2,T_3$ be measurable random variables in a finite abelian group with $T_1+T_2+T_3=0$, and set $\delta=I[T_1:T_2]+I[T_1:T_3]+I[T_2:T_3]$. For any measurable $Y_1,\ldots,Y_n$ and any $\alpha>0$, there is a measurable random variable $U$ such that $d[U;U]+\alpha\sum_{i=1}^n d[Y_i;U]\le\left(2+\frac{\alpha n}{2}\right)\delta+\alpha\sum_{i=1}^n d[Y_i;T_2].$