mem_map — Mathlib

English

The relation between lists and their cyclic coe-classes: l ∈ s.lists iff (l : Cycle α) = s.

Русский

Связь между списками и их циклами-коэффициентами: l ∈ s.lists тогда и только тогда, когда (l : Cycle α) = s.

LaTeX

$$$l \in s.lists \iff (l : Cycle\, α) = s$$$

Lean4

@[simp]
theorem mem_map {β : Type*} {f : α → β} {b : β} {s : Cycle α} : b ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b :=
  Quotient.inductionOn' s (by simp)

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