pairwiseDisjoint_image — Mathlib

English

If g is injective on s, then (g '' s).PairwiseDisjoint f is equivalent to s.PairwiseDisjoint (f ∘ g).

Русский

Если g инъективна на s, то (g[s]).PairwiseDisjoint f эквивалентно s.PairwiseDisjoint (f ∘ g).

LaTeX

$$∀ {g : ι' → ι}, h : s.InjOn g → (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g)$$

Lean4

theorem pairwiseDisjoint_image {g : ι' → ι} {s : Set ι'} (h : s.InjOn g) :
    (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g) :=
  h.pairwise_image

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