mem_sym2_iff_subset — Mathlib

English

An element z of Sym2 α lies in s.sym2 if and only if the underlying set of z is a subset of s.

Русский

Элемент z из Sym2 α принадлежит s.sym2 тогда и только тогда, когда множество z является подмножеством s.

LaTeX

$$$\\forall {z : \\mathrm{Sym}^2(\\alpha)}\\; z \\in s.sym2 \\Leftrightarrow (z:\\mathrm{Set}\\,\\alpha) \\subseteq s$$$

Lean4

theorem mem_sym2_iff_subset {z : Sym2 α} : z ∈ s.sym2 ↔ (z : Set α) ⊆ s :=
  by
  induction z using Sym2.inductionOn
  simp [pair_subset_iff]

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