instNeBotNhdsWithinIio — Mathlib

English

If nhdsWithin x in the upper ray Ioi x is nontrivial, then nhdsWithin (toDual x) in the lower ray Iio (toDual x) is nontrivial.

Русский

Если nhdsWithin x на верхнем луче Ioi x не тривиальна, то nhdsWithin (toDual x) на нижнем луче Iio (toDual x) не тривиальна.

LaTeX

$$$ (\\nhdsWithin x \\ Ioi x).NeBot \\Rightarrow (\\nhdsWithin (\\mathrm{toDual}~x) \\ Iio (\\mathrm{toDual}~x)).NeBot. $$$

Lean4

instance instNeBotNhdsWithinIio [(𝓝[>] x).NeBot] : (𝓝[<] toDual x).NeBot :=
  ‹_›

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