instOrderClosedTopology — Mathlib

English

If f → a1 and g → a2 along b, and f x ≤ g x for all x, then a1 ≤ a2.

Русский

Если f сходится к a1 и g сходится к a2 вдоль b, и для всех x выполняется f(x) ≤ g(x), то a1 ≤ a2.

LaTeX

$$$\text{Tendsto } f b (\mathcal{N} a_1) \land \text{Tendsto } g b (\mathcal{N} a_2) \land \forall x, f(x) \le g(x) \Rightarrow a_1 \le a_2$$$

Lean4

instance {p : α → Prop} : OrderClosedTopology (Subtype p) :=
  have this : Continuous fun p : Subtype p × Subtype p => ((p.fst : α), (p.snd : α)) :=
    continuous_subtype_val.prodMap continuous_subtype_val
  OrderClosedTopology.mk (t.isClosed_le'.preimage this)

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