sigmaLift_nonempty — Mathlib

English

sigmaLift f a b is nonempty precisely when a and b have the same index and the corresponding f(a,b) is nonempty.

Русский

sigmaLift f a b непуст тогда и только тогда, когда a и b имеют одинаковый индекс, и соответствующее f(a,b) непусто.

LaTeX

$$$$ \sigmaLift f a b \neq \emptyset \;\iff\; \exists h : a.1 = b.1, (f (h \|> a.2) b.2).\text{Nonempty} $$$$

Lean4

theorem sigmaLift_nonempty : (sigmaLift f a b).Nonempty ↔ ∃ h : a.1 = b.1, (f (h ▸ a.2) b.2).Nonempty :=
  by
  simp_rw [nonempty_iff_ne_empty, sigmaLift]
  split_ifs with h <;> simp [h]

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