exists_mem_and_apply_eq_iff — Mathlib

English

If f is involutive, then for any x and any list l, there exists y ∈ l with f y = x if and only if f x ∈ l.

Русский

Если f — инволютивная функция, то для любого x и списка l существует y ∈ l такие, что f y = x, тогда и только тогда f x ∈ l.

LaTeX

$$Involutive f → ∀ x l, (∃ y ∈ l, f y = x) ⇔ f x ∈ l$$

Lean4

@[simp]
theorem _root_.Function.Involutive.exists_mem_and_apply_eq_iff {f : α → α} (hf : Function.Involutive f) (x : α)
    (l : List α) : (∃ y : α, y ∈ l ∧ f y = x) ↔ f x ∈ l :=
  ⟨by rintro ⟨y, h, rfl⟩; rwa [hf y], fun h => ⟨f x, h, hf _⟩⟩

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