103theorem affineShift_mem_LevelSet {n : ℕ} (α : Vec n) {c s : ℝ} {t v : Vec n} 104 (ht : t ∈ LevelSet α c) (hv : v ∈ Radical α) : 105 affineShift t v s ∈ LevelSet α c := by
proof body
Term-mode proof.
106 rw [mem_LevelSet_iff] at ht ⊢ 107 have hv' : dot α v = 0 := hv 108 rw [dot_affineShift, ht, hv'] 109 ring 110 111/-- The radical distribution is integrable: its integral leaves are the affine 112hyperplanes `dot α = c`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.