equal
deleted
inserted
replaced
800 let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)" |
800 let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)" |
801 have "?z \<in> approximants w" |
801 have "?z \<in> approximants w" |
802 by (simp add: approximants_def approx_below) |
802 by (simp add: approximants_def approx_below) |
803 moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z" |
803 moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z" |
804 by (simp add: approximants_def compact_le_def) |
804 by (simp add: approximants_def compact_le_def) |
805 (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2) |
805 (metis i j monofun_cfun chain_mono chain_approx max.cobounded1 max.cobounded2) |
806 ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. |
806 ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. |
807 next |
807 next |
808 fix x y :: "'a compact_basis" |
808 fix x y :: "'a compact_basis" |
809 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" |
809 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" |
810 unfolding approximants_def compact_le_def |
810 unfolding approximants_def compact_le_def |