Zulip Chat Archive

Stream: new members

Topic: Reflection of z in a1 about a1


Shadman Sakib (Aug 20 2021 at 02:21):

How do I show that reflection a1 of z = z, where z is in a1?

Shadman Sakib (Aug 20 2021 at 02:21):

import analysis.complex.circle
import analysis.normed_space.inner_product

noncomputable theory

open complex
variables {V : Type*} [inner_product_space  V]

lemma same_point (a₁ : subspace  V) [complete_space a₁] (z : V) (h: z  a₁) : reflection (a₁) z = z :=
begin
  sorry,
end

Kyle Miller (Aug 20 2021 at 02:29):

I'm not sure if it's because I don't have the same version of mathlib, but I don't seem to have reflection. Where is it defined?

Shadman Sakib (Aug 20 2021 at 02:37):

Ah yeah, you know what, someone is adding reflection to the library. I have their version of math lib, sorry

Shadman Sakib (Aug 20 2021 at 02:38):

I will update this stream when reflection is added


Last updated: Dec 20 2023 at 11:08 UTC