isClosed_le_of_isClosed_nonneg — Mathlib

English

If {x ∈ α : 0 ≤ x} is closed, then the set { (p,q) ∈ α×α : p ≤ q } is closed.

Русский

Если множество {x : 0 ≤ x} замкнуто, то множество { (p,q) ∈ α×α : p ≤ q } замкнуто.

LaTeX

$$$\{(p,q) \in \alpha \times \alpha : p \le q\}$ is closed$$

Lean4

theorem isClosed_le_of_isClosed_nonneg {G} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G]
    [ContinuousSub G] (h : IsClosed {x : G | 0 ≤ x}) : IsClosed {p : G × G | p.fst ≤ p.snd} :=
  by
  have : {p : G × G | p.fst ≤ p.snd} = (fun p : G × G => p.snd - p.fst) ⁻¹' {x : G | 0 ≤ x} := by ext1 p;
    simp only [sub_nonneg, Set.preimage_setOf_eq]
  rw [this]
  exact IsClosed.preimage (continuous_snd.sub continuous_fst) h

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