bind_comp — Mathlib

English

If S f holds and R h1 g holds, then the bind of S and R along g∘f exists and is obtained by the expected data.

Русский

Если выполняются условия S f и R h1 g, то существует связывание S и R над g∘f и получаемое выражение задаётся данными.

LaTeX

$$$\\text{bind } S\\; R\\; (g\\circ f) = \\langle \\text{Y}, \\text{g}, \\text{f}, \\text{hf}, \\text{hg}, \\text{rfl} \\rangle$ provided \$h_1: S f\$ and \$h_2: R(h_1) g\$.$$

Lean4

@[simp]
theorem bind_comp {S : Presieve X} {R : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → Presieve Y} {g : Z ⟶ Y} (h₁ : S f) (h₂ : R h₁ g) :
    bind S R (g ≫ f) :=
  ⟨_, _, _, h₁, h₂, rfl⟩
    -- Note we can't make this into `HasSingleton` because of the out-param.

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