sumSet_preimage_inr — Mathlib

English

Let s and t be disjoint subsets of α. Then the preimage under inr of the sumSet h preimage r equals r ∩ t.

Русский

Пусть s и t — попарно непересекающиеся подмножества α. Тогда предобразование по inr от (sumSet h)^{-1}(r) равно r ∩ t.

LaTeX

$$$\\operatorname{inr}^{-1}\\bigl( (\\operatorname{sumSet}h)^{-1}(r) \\bigr) = r \\cap t.$$$

Lean4

@[simp]
theorem sumSet_preimage_inr (h : Disjoint s t) : .inr ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ t := by
  simp [Set.ext_iff]

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