inter_preimage_val_iff — Mathlib

English

The inclusion map is an open embedding under suitable subset relations and openness assumptions.

Русский

Включение является открытым вложением при подходящем отношении подмножеств и открытости.

LaTeX

$$$\\forall hst,\\; \\text{IsOpenEmbedding}(\\text{inclusion}(hst)).$$$

Lean4

@[simp]
theorem inter_preimage_val_iff {s t : Set X} (hs : IsOpen s) : IsOpen (s ↓∩ t) ↔ IsOpen (s ∩ t) :=
  ⟨fun h ↦ by simpa using hs.isOpenMap_subtype_val _ h, fun h ↦
    (Subtype.preimage_coe_self_inter _ _).symm ▸ h.preimage_val⟩

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