English
cardinality of the sigma-lifted Icc set satisfies a conditional depending on whether a and b have the same first component; if they do, the fiber cardinality is the corresponding Icc in the fiber; otherwise zero.
Русский
Мощность множества Icc над сигма-типом оказывается равной 0 если первые компоненты различны, иначе равна мощности Icc в соответствующем сомножителе.
LaTeX
$$$\\#(Icc a b) = \\operatorname{if} h : a.\\mathrm{fst} = b.\\mathrm{fst} \\ \\operatorname{then} \\ # (Icc (h.rec a.2) b.2) \\operatorname{else} 0$$$
Lean4
instance instLocallyFiniteOrder : LocallyFiniteOrder (Σ i, α i)
where
finsetIcc := sigmaLift fun _ => Icc
finsetIco := sigmaLift fun _ => Ico
finsetIoc := sigmaLift fun _ => Ioc
finsetIoo := sigmaLift fun _ => Ioo
finset_mem_Icc := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ =>
by
simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
finset_mem_Ico := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ =>
by
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ← exists_prop]
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
finset_mem_Ioc := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ =>
by
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ← exists_prop]
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
finset_mem_Ioo := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ =>
by
simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
