sigmaLift_eq_empty — Mathlib

English

The sigmaLift is empty if and only if, for every possible equality h between the indices, f(recursively transported) is empty.

Русский

SigmaLift пуст, если и только если для каждого равенства индексов h функция f после переноса по h пустая.

LaTeX

$$$$ \sigmaLift f a b = \emptyset \iff \forall h : a.1 = b.1, f (\mathrm{Eq.rec} \; a.2 \; h) b.2 = \emptyset $$$$

Lean4

theorem sigmaLift_eq_empty : sigmaLift f a b = ∅ ↔ ∀ h : a.1 = b.1, f (h ▸ a.2) b.2 = ∅ :=
  by
  simp_rw [sigmaLift]
  split_ifs with h
  · simp [h]
  · simp [h]

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