image_of_le — Mathlib

English

If s is pairwise disjoint under f and f ∘ g ≤ f, then (g '' s) is PairwiseDisjoint under f.

Русский

Если s попарно непересекается по f и f ∘ g ≤ f, то g[s] попарно непересекается по f.

LaTeX

$$hs : s.PairwiseDisjoint f \\Rightarrow (g \\text{ '' } s).PairwiseDisjoint f$$

Lean4

theorem image_of_le (hs : s.PairwiseDisjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) : (g '' s).PairwiseDisjoint f :=
  by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h
  exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

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