norm_pos_iff' etc

Stream: maths

[Yury G. Kudryashov]

Hi @Patrick Massot, I see that the commit message of #7858 says that docs#norm_pos_iff' is useful sometimes in LTE. Could you please provide more details? E.g., is it hard to write something like

  letI : normed_group E := of_semi_normed_group_t2 E,

in the proof? Here of_semi_normed_group_t2 can be defined as

def of_semi_normed_group_t2 (E : Type*) [semi_normed_group E] [separated E] :
  normed_group E :=
{ to_metric_space := of_t2_pseudo_metric_space ‹_›, .. ‹semi_normed_group E› }

[Yury G. Kudryashov]

Or we can write a tactic that upgrades pseudo_metric_space/semi_normed_* to metric_space/normed_* provided that the environment has [separated E] (or [t2_space E]).

[Patrick Massot]

Yes, we could adjust LTE if you provide of_semi_normed_group_t2 in the same PR removing this lemma.

[Patrick Massot]

@Johan Commelin if this happens then you need to start this proof with letI : ∀ c i, normed_group (C c i) := λ c i, of_semi_normed_group_t2 _,

[Johan Commelin]

Thanks for the heads up!