Theorems · Theorem · logic and foundations

PFun.mem_fix_iff

∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β},
  b ∈ f.fix a ↔ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Defined in

Mathlib.Data.PFun

Cited by

6 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound