instNeBotNhdsWithinIoi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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