inj_on_iUnion_of_directed — Mathlib

English

If a family s_i of subsets is directed by inclusion, and f is injOn on each s_i, then f is injOn on the union.

Русский

Если семейство подмножеств s_i упорядочено по включению и f инъективно на каждом s_i, то f инъективно на объединении.

LaTeX

$$$\\text{InjOn}(f, \\bigcup_i s_i)$, given directedness and each injOn.$$

Lean4

theorem inj_on_iUnion_of_directed {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {f : α → β} (hf : ∀ i, InjOn f (s i)) :
    InjOn f (⋃ i, s i) := by
  intro x hx y hy hxy
  rcases mem_iUnion.1 hx with ⟨i, hx⟩
  rcases mem_iUnion.1 hy with ⟨j, hy⟩
  rcases hs i j with ⟨k, hi, hj⟩
  exact hf k (hi hx) (hj hy) hxy

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