mem_sigma — Mathlib

English

For all p : Σ a, σ a, p ∈ s.sigma t iff p.1 ∈ s ∧ p.2 ∈ t p.1.

Русский

Для любого p : Σ a, σ a, p ∈ s.sigma t тогда и только тогда, когда p.1 ∈ s и p.2 ∈ t(p.1).

LaTeX

$$$\forall {p : \Sigma a, \sigma a},\ p \in s.\sigma t \iff p.1 \in s \wedge p.2 \in t p.1$$$

Lean4

@[simp]
theorem mem_sigma : ∀ {p : Σ a, σ a}, p ∈ @Multiset.sigma α σ s t ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
  | ⟨a, b⟩ => by simp [Multiset.sigma, and_left_comm]

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