English
For any nonempty α, a SetRel r is not finite dimensional if and only if it is infinite dimensional.
Русский
Для любого непустого множества α множество отношений r не конечнодименсионально тогда и только тогда, когда оно бесконечно размерно.
LaTeX
$$$$ \\neg \\operatorname{FiniteDimensional}(r) \\iff \\operatorname{InfiniteDimensional}(r). $$$$
Lean4
theorem not_finiteDimensional_iff [Nonempty α] : ¬r.FiniteDimensional ↔ r.InfiniteDimensional :=
by
rw [finiteDimensional_iff, infiniteDimensional_iff]
push_neg
constructor
· intro H n
induction n with
| zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
| succ n IH =>
obtain ⟨l, hl⟩ := IH
obtain ⟨l', hl'⟩ := H l
exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩
· intro H l
obtain ⟨l', hl'⟩ := H (l.length + 1)
exact ⟨l', by simp [hl']⟩
