instHImp — Mathlib

English

There is a Heyting implication on CompactOpens α, giving a notion of relative openness/implication.

Русский

Существует импликация Хайтинга на CompactOpens α, задающая отношение импликации над множествами.

LaTeX

$$HImp(CompactOpens(α))$$

Lean4

instance instHImp : HImp (CompactOpens α) where
  himp s
    t :=
    ⟨⟨s ⇨ t, IsClosed.isCompact (by simpa [himp_eq] using t.isCompact.isClosed.union s.isOpen.isClosed_compl)⟩, by
      simpa [himp_eq] using t.isOpen.union s.isCompact.isClosed.isOpen_compl⟩

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