disjoint_val_image — Mathlib

English

The image of a set under Subtype.val is disjoint from the original set, reflecting the complement structure.

Русский

Образ множества при помощи Subtype.val является дизъюнктным по отношению к исходному множеству, отражая структуру дополнения.

LaTeX

$$Disjoint s (Subtype.val '' t)$$

Lean4

@[to_additive]
theorem disjoint_val_image {t : Set (ofFixingSubgroup M s)} : Disjoint s (Subtype.val '' t) :=
  by
  rw [Set.disjoint_iff]
  rintro a ⟨hbs, ⟨b, _, rfl⟩⟩; exact (b.prop hbs).elim

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