preimage_val_subset_preimage_val_iff

English

Subset relation between preimages under Subtype.val is equivalent to subset relation of intersections with s.

Русский

Подмножество между предобразами Subtype.val эквивалентно вложению пересечений с s.

LaTeX

$$$ (\text{Set.instHasSubset.Subset} (Set.preimage Subtype.val t) (Set.preimage Subtype.val u)) \iff (s \cap t \subseteq s \cap u) $$$

Lean4

theorem preimage_val_subset_preimage_val_iff (s t u : Set α) :
    (Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u :=
  by
  constructor
  · rw [← image_preimage_coe, ← image_preimage_coe]
    exact image_mono
  · intro h x a
    exact (h ⟨x.2, a⟩).2

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