mem_sigma_iff — Mathlib

English

Membership in the sigma is equivalent to membership in the first coordinate set and in the corresponding second set.

Русский

Членство в sigma эквивалентно членству в первом множестве-координате и во втором соответствующем множестве.

LaTeX

$$$x \\in s.\\sigma t \\iff x.1 \\in s \\land x.2 \\in t(x.1)$$$

Lean4

@[simp, grind =]
theorem mem_sigma_iff : x ∈ s.sigma t ↔ x.1 ∈ s ∧ x.2 ∈ t x.1 :=
  Iff.rfl

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