Ici_mem_nhdsSet_Ici_iff — Mathlib

English

Under NeBot assumption for nhds within b, Ici a ∈ 𝓝ˢ(Ici b) iff a < b.

Русский

При условии NeBot для nhds внутри b: Ici a ∈ 𝓝ˢ(Ici b) тогда и только если a < b.

LaTeX

$$$[NeBot(𝓝[<] b)] : Ici\ a ∈ 𝓝ˢ(Ici\ b) \iff a < b$$$

Lean4

@[simp]
theorem Ici_mem_nhdsSet_Ici_iff {a b : α} [NeBot (𝓝[<] b)] : Ici a ∈ 𝓝ˢ (Ici b) ↔ a < b :=
  have : NeBot (𝓝[>] (toDual b)) := ‹_›;
  Iic_mem_nhdsSet_Iic_iff (a := toDual a) (b := toDual b)

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