ne_of_mem_slice — Mathlib

English

Elements in distinct slices are distinct; if A1 ∈ 𝒜_{r1} and A2 ∈ 𝒜_{r2} with r1 ≠ r2, then A1 ≠ A2.

Русский

Элементы в разных срезах различны; если A1 ∈ 𝒜_{r1}, A2 ∈ 𝒜_{r2} и r1 ≠ r2, то A1 ≠ A2.

LaTeX

$$$ r_1 \neq r_2 \Rightarrow A_1 \neq A_2 \text{ if } A_i \in 𝒜_{r_i} $$$

Lean4

/-- Elements in distinct slices must be distinct. -/
theorem ne_of_mem_slice (h₁ : A₁ ∈ 𝒜 #r₁) (h₂ : A₂ ∈ 𝒜 #r₂) : r₁ ≠ r₂ → A₁ ≠ A₂ :=
  mt fun h => (sized_slice h₁).symm.trans ((congr_arg card h).trans (sized_slice h₂))

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