isClosed_imp — Mathlib

English

If the set {x | p(x)} is open and the set {x | q(x)} is closed, then the set {x | p(x) → q(x)} is closed.

Русский

Если множество {x | p(x)} открыто и множество {x | q(x)} замкнуто, то множество {x | p(x) → q(x)} замкнуто.

LaTeX

$$$\operatorname{IsOpen}(\{x \mid p(x)\}) \Rightarrow \operatorname{IsClosed}(\{x \mid q(x)\}) \Rightarrow \operatorname{IsClosed}(\{x \mid p(x) \to q(x)\})$$$

Lean4

theorem isClosed_imp {p q : X → Prop} (hp : IsOpen {x | p x}) (hq : IsClosed {x | q x}) : IsClosed {x | p x → q x} := by
  simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq

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