of_downward_closed — Mathlib

English

For any f, the equality-based composition equals the right-hand-side relation.

Русский

Для любого f композиция через равенство равна правой части отношения.

LaTeX

$$$\forall r:\alpha\to\beta\to \mathrm{Prop},\; (r \circ_r (\cdot = f \cdot)) = (r \cdot <| f \cdot)$$$

Lean4

theorem _root_.Acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b) (a : α) (ha : Acc (InvImage rβ f) a) :
    Acc rβ (f a) :=
  ha.of_fibration f fun a _ h ↦
    let ⟨a', he⟩ := dc h
    ⟨a', by simp_all [InvImage], he⟩

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