sigmaToiUnion_injective — Mathlib

English

If t is pairwise disjoint (on t), then sigmaToiUnion t is injective.

Русский

Если family t разбивают на непересекающиеся части, тогда σToiUnion t инъективно.

LaTeX

$$$$\\text{If } t \\text{ is pairwise disjoint, then } \\text{sigmaToiUnion } t \\text{ is injective}. $$$$

Lean4

theorem sigmaToiUnion_injective (h : Pairwise (Disjoint on t)) : Injective (sigmaToiUnion t)
  | ⟨a₁, b₁, h₁⟩, ⟨a₂, b₂, h₂⟩, eq =>
    have b_eq : b₁ = b₂ := congr_arg Subtype.val eq
    have a_eq : a₁ = a₂ :=
      by_contradiction fun ne =>
        have : b₁ ∈ t a₁ ∩ t a₂ := ⟨h₁, b_eq.symm ▸ h₂⟩
        (h ne).le_bot this
    Sigma.eq a_eq <| Subtype.eq <| by subst b_eq; subst a_eq; rfl

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