equal
deleted
inserted
replaced
184 by (auto simp: span_base) |
184 by (auto simp: span_base) |
185 |
185 |
186 lemma span_zero: "0 \<in> span S" |
186 lemma span_zero: "0 \<in> span S" |
187 by (auto simp: span_explicit intro!: exI[of _ "{}"]) |
187 by (auto simp: span_explicit intro!: exI[of _ "{}"]) |
188 |
188 |
189 lemma span_UNIV: "span UNIV = UNIV" |
189 lemma span_UNIV[simp]: "span UNIV = UNIV" |
190 by (auto intro: span_base) |
190 by (auto intro: span_base) |
191 |
191 |
192 lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S" |
192 lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S" |
193 unfolding span_explicit |
193 unfolding span_explicit |
194 proof safe |
194 proof safe |