English
Assuming a nonempty family of coordinates, cylinder s S is empty if and only if S is empty.
Русский
При условии не пустого семейства координат цилиндр s S бесконечен тогда, когда S пусто.
LaTeX
$$$$\\text{cylinder}(s,S) = \\emptyset \\iff S = \\emptyset.$$$$
Lean4
@[simp]
theorem cylinder_eq_empty_iff [h_nonempty : Nonempty (∀ i, α i)] (s : Finset ι) (S : Set (∀ i : s, α i)) :
cylinder s S = ∅ ↔ S = ∅ :=
by
refine ⟨fun h ↦ ?_, fun h ↦ by (rw [h]; exact cylinder_empty _)⟩
by_contra hS
rw [← Ne, ← nonempty_iff_ne_empty] at hS
let f := hS.some
have hf : f ∈ S := hS.choose_spec
classical
let f' : ∀ i, α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
have hf' : f' ∈ cylinder s S := by
rw [mem_cylinder]
simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
rw [h] at hf'
exact notMem_empty _ hf'
