liftRelAux_inr_inl — Mathlib

English

Relation on Sum.inl a and destruct cb equals existence of b in cb with R a b, under Ret-left semantics.

Русский

Связь LiftRelAux между Sum.inl a и дескрем cb равна существованию b в cb с R a b, в рамках левого случая.

LaTeX

$$$\\forall a\\in\\alpha,\\text{LiftRelAux }R C (\\mathrm{Sum.inl}\\ a)(\\mathrm{destruct}\\ cb) \\iff \\exists b\\in cb\\, R\\ a\\ b$$$

Lean4

@[simp]
theorem liftRelAux_inr_inl {b : β} {ca} : LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a, a ∈ ca ∧ R a b :=
  rfl

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